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

Metamath Proof Explorer

Theorem sbralieALT

Description: Alternative shorter proof of sbralie dependent on ax-ext , df-cleq , df-clel . (Contributed by NM, 5-Sep-2004) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis sbralie.1 ⊢ x = y → φ ↔ ψ
Assertion sbralieALT ⊢ ∀ x ∈ y φ ↔ y x ∀ y ∈ x ψ

Proof

Step Hyp Ref Expression
1 sbralie.1 ⊢ x = y → φ ↔ ψ
2 cbvralsvw ⊢ ∀ y ∈ x ψ ↔ ∀ z ∈ x z y ψ
3 2 sbbii ⊢ y x ∀ y ∈ x ψ ↔ y x ∀ z ∈ x z y ψ
4 raleq ⊢ x = y → ∀ z ∈ x z y ψ ↔ ∀ z ∈ y z y ψ
5 4 sbievw ⊢ y x ∀ z ∈ x z y ψ ↔ ∀ z ∈ y z y ψ
6 cbvralsvw ⊢ ∀ z ∈ y z y ψ ↔ ∀ x ∈ y x z z y ψ
7 sbco2vv ⊢ x z z y ψ ↔ x y ψ
8 1 bicomd ⊢ x = y → ψ ↔ φ
9 8 equcoms ⊢ y = x → ψ ↔ φ
10 9 sbievw ⊢ x y ψ ↔ φ
11 7 10 bitri ⊢ x z z y ψ ↔ φ
12 11 ralbii ⊢ ∀ x ∈ y x z z y ψ ↔ ∀ x ∈ y φ
13 6 12 bitri ⊢ ∀ z ∈ y z y ψ ↔ ∀ x ∈ y φ
14 3 5 13 3bitrri ⊢ ∀ x ∈ y φ ↔ y x ∀ y ∈ x ψ