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 ⊢ x y | φ = x y | ψ ↔ ∀ x ∀ y φ ↔ ψ

Proof

Step Hyp Ref Expression
1 ssopab2bw ⊢ x y | φ ⊆ x y | ψ ↔ ∀ x ∀ y φ → ψ
2 ssopab2bw ⊢ x y | ψ ⊆ x y | φ ↔ ∀ x ∀ y ψ → φ
3 1 2 anbi12i ⊢ x y | φ ⊆ x y | ψ ∧ x y | ψ ⊆ x y | φ ↔ ∀ x ∀ y φ → ψ ∧ ∀ x ∀ y ψ → φ
4 eqss ⊢ x y | φ = x y | ψ ↔ x y | φ ⊆ x y | ψ ∧ x y | ψ ⊆ x y | φ
5 2albiim ⊢ ∀ x ∀ y φ ↔ ψ ↔ ∀ x ∀ y φ → ψ ∧ ∀ x ∀ y ψ → φ
6 3 4 5 3bitr4i ⊢ x y | φ = x y | ψ ↔ ∀ x ∀ y φ ↔ ψ