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

Metamath Proof Explorer

Theorem eqopab2bw

Description: Equivalence of ordered pair abstraction equality and biconditional. Version of eqopab2b with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 4-Jan-2017) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Assertion eqopab2bw ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 ssopab2bw ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) )
2 ssopab2bw ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜓 → 𝜑 ) )
3 1 2 anbi12i ⊢ ( ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝜓 → 𝜑 ) ) )
4 eqss ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ∧ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ) )
5 2albiim ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ 𝜓 ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → 𝜓 ) ∧ ∀ 𝑥 ∀ 𝑦 ( 𝜓 → 𝜑 ) ) )
6 3 4 5 3bitr4i ⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ↔ ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ 𝜓 ) )