Theorem opelopab3

Description: Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011)

	Ref	Expression
Hypotheses	opelopab3.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
	opelopab3.2	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
	opelopab3.3	⊢ ( 𝜒 → 𝐴 ∈ 𝐶 )
Assertion	opelopab3	⊢ ( 𝐵 ∈ 𝐷 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		opelopab3.1	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
2		opelopab3.2	⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
3		opelopab3.3	⊢ ( 𝜒 → 𝐴 ∈ 𝐶 )
4		elopaelxp	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) )
5		opelxp1	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) → 𝐴 ∈ V )
6	4 5	syl	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } → 𝐴 ∈ V )
7	6	anim1i	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐷 ) )
8	7	ancoms	⊢ ( ( 𝐵 ∈ 𝐷 ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐷 ) )
9	3	elexd	⊢ ( 𝜒 → 𝐴 ∈ V )
10	9	anim1i	⊢ ( ( 𝜒 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐷 ) )
11	10	ancoms	⊢ ( ( 𝐵 ∈ 𝐷 ∧ 𝜒 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐷 ) )
12	1 2	opelopabg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐷 ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 ) )
13	8 11 12	pm5.21nd	⊢ ( 𝐵 ∈ 𝐷 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 ) )