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

Metamath Proof Explorer

Theorem ssopab2bw

Description: Equivalence of ordered pair abstraction subclass and implication. Version of ssopab2b with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 27-Dec-1996) Avoid ax-13 . (Revised by GG, 26-Jan-2024)

Ref Expression
Assertion ssopab2bw ⊢ x y | φ ⊆ x y | ψ ↔ ∀ x ∀ y φ → ψ

Proof

Step Hyp Ref Expression
1 nfopab1 ⊢ Ⅎ _ x x y | φ
2 nfopab1 ⊢ Ⅎ _ x x y | ψ
3 1 2 nfss ⊢ Ⅎ x x y | φ ⊆ x y | ψ
4 nfopab2 ⊢ Ⅎ _ y x y | φ
5 nfopab2 ⊢ Ⅎ _ y x y | ψ
6 4 5 nfss ⊢ Ⅎ y x y | φ ⊆ x y | ψ
7 ssel ⊢ x y | φ ⊆ x y | ψ → x y ∈ x y | φ → x y ∈ x y | ψ
8 opabidw ⊢ x y ∈ x y | φ ↔ φ
9 opabidw ⊢ x y ∈ x y | ψ ↔ ψ
10 7 8 9 3imtr3g ⊢ x y | φ ⊆ x y | ψ → φ → ψ
11 6 10 alrimi ⊢ x y | φ ⊆ x y | ψ → ∀ y φ → ψ
12 3 11 alrimi ⊢ x y | φ ⊆ x y | ψ → ∀ x ∀ y φ → ψ
13 ssopab2 ⊢ ∀ x ∀ y φ → ψ → x y | φ ⊆ x y | ψ
14 12 13 impbii ⊢ x y | φ ⊆ x y | ψ ↔ ∀ x ∀ y φ → ψ