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	⊢ ( 𝐴 ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → 𝜒 )