Metamath Proof Explorer

Theorem sbralie

Description: Implicit to explicit substitution that swaps variables in a rectrictedly universally quantified expression. (Contributed by NM, 5-Sep-2004) Avoid ax-ext . (Revised by Wolf Lammen, 10-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 sbralie.1 ⊢ x = y → φ ↔ ψ
2 df-ral ⊢ ∀ x ∈ y φ ↔ ∀ x x ∈ y → φ
3 sbim ⊢ y z x ∈ z → φ ↔ y z x ∈ z → y z φ
4 elsb2 ⊢ y z x ∈ z ↔ x ∈ y
5 sbv ⊢ y z φ ↔ φ
6 4 5 imbi12i ⊢ y z x ∈ z → y z φ ↔ x ∈ y → φ
7 3 6 bitri ⊢ y z x ∈ z → φ ↔ x ∈ y → φ
8 7 albii ⊢ ∀ x y z x ∈ z → φ ↔ ∀ x x ∈ y → φ
9 elequ1 ⊢ x = y → x ∈ z ↔ y ∈ z
10 9 1 imbi12d ⊢ x = y → x ∈ z → φ ↔ y ∈ z → ψ
11 10 cbvalvw ⊢ ∀ x x ∈ z → φ ↔ ∀ y y ∈ z → ψ
12 df-ral ⊢ ∀ y ∈ x ψ ↔ ∀ y y ∈ x → ψ
13 12 sbbii ⊢ z x ∀ y ∈ x ψ ↔ z x ∀ y y ∈ x → ψ
14 sbal ⊢ z x ∀ y y ∈ x → ψ ↔ ∀ y z x y ∈ x → ψ
15 sbim ⊢ z x y ∈ x → ψ ↔ z x y ∈ x → z x ψ
16 elsb2 ⊢ z x y ∈ x ↔ y ∈ z
17 sbv ⊢ z x ψ ↔ ψ
18 16 17 imbi12i ⊢ z x y ∈ x → z x ψ ↔ y ∈ z → ψ
19 15 18 bitri ⊢ z x y ∈ x → ψ ↔ y ∈ z → ψ
20 19 albii ⊢ ∀ y z x y ∈ x → ψ ↔ ∀ y y ∈ z → ψ
21 13 14 20 3bitrri ⊢ ∀ y y ∈ z → ψ ↔ z x ∀ y ∈ x ψ
22 11 21 bitri ⊢ ∀ x x ∈ z → φ ↔ z x ∀ y ∈ x ψ
23 22 sbbii ⊢ y z ∀ x x ∈ z → φ ↔ y z z x ∀ y ∈ x ψ
24 sbal ⊢ y z ∀ x x ∈ z → φ ↔ ∀ x y z x ∈ z → φ
25 sbco2vv ⊢ y z z x ∀ y ∈ x ψ ↔ y x ∀ y ∈ x ψ
26 23 24 25 3bitr3i ⊢ ∀ x y z x ∈ z → φ ↔ y x ∀ y ∈ x ψ
27 2 8 26 3bitr2i ⊢ ∀ x ∈ y φ ↔ y x ∀ y ∈ x ψ