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

Metamath Proof Explorer

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 bitrid ⊢ ( ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜒 ) )