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 , df-cleq , df-clel . (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 nfv ⊢ Ⅎ z φ
4 3 sblim ⊢ y z x ∈ z → φ ↔ y z x ∈ z → φ
5 elsb2 ⊢ y z x ∈ z ↔ x ∈ y
6 5 imbi1i ⊢ y z x ∈ z → φ ↔ x ∈ y → φ
7 4 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 nfv ⊢ Ⅎ x ψ
16 15 sblim ⊢ z x y ∈ x → ψ ↔ z x y ∈ x → ψ
17 elsb2 ⊢ z x y ∈ x ↔ y ∈ z
18 17 imbi1i ⊢ z x y ∈ x → ψ ↔ y ∈ z → ψ
19 16 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 ψ