Theorem opelopabt

Description: Closed theorem form of opelopab . (Contributed by NM, 19-Feb-2013)

	Ref	Expression
Assertion	opelopabt	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		elopab	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
2		19.26-2	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) )
3		anim12	⊢ ( ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜓 ↔ 𝜒 ) ) ) )
4		bitr	⊢ ( ( ( 𝜑 ↔ 𝜓 ) ∧ ( 𝜓 ↔ 𝜒 ) ) → ( 𝜑 ↔ 𝜒 ) )
5	3 4	syl6	⊢ ( ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜒 ) ) )
6	5	2alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜒 ) ) )
7	2 6	sylbir	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜒 ) ) )
8		copsex2t	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜒 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ 𝜒 ) )
9	7 8	stoic3	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ 𝜒 ) )
10	1 9	syl5bb	⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 ) )