This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elopabi

Description: A consequence of membership in an ordered-pair class abstraction, using ordered pair extractors. (Contributed by NM, 29-Aug-2006)

Ref Expression
Hypotheses elopabi.1 ⊢ ( 𝑥 = ( 1st ‘ 𝐴 ) → ( 𝜑 ↔ 𝜓 ) )
elopabi.2 ⊢ ( 𝑦 = ( 2nd ‘ 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion elopabi ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → 𝜒 )

Proof

Step Hyp Ref Expression
1 elopabi.1 ⊢ ( 𝑥 = ( 1st ‘ 𝐴 ) → ( 𝜑 ↔ 𝜓 ) )
2 elopabi.2 ⊢ ( 𝑦 = ( 2nd ‘ 𝐴 ) → ( 𝜓 ↔ 𝜒 ) )
3 relopabv ⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
4 1st2nd ⊢ ( ( Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
5 3 4 mpan ⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
6 id ⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
7 5 6 eqeltrrd ⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
8 fvex ⊢ ( 1st ‘ 𝐴 ) ∈ V
9 fvex ⊢ ( 2nd ‘ 𝐴 ) ∈ V
10 8 9 1 2 opelopab ⊢ ( ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 )
11 7 10 sylib ⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → 𝜒 )