Metamath Proof Explorer

Theorem sbralie

Description: Implicit to explicit substitution that swaps variables in a restrictedly universally quantified expression. (Contributed by NM, 5-Sep-2004) Avoid ax-ext , df-cleq , df-clel . (Revised by Wolf Lammen, 10-Mar-2025) Avoid ax-10 , ax-12 . (Revised by SN, 13-Nov-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 elequ2 ⊢ z = y → x ∈ z ↔ x ∈ y
4 3 imbi1d ⊢ z = y → x ∈ z → φ ↔ x ∈ y → φ
5 4 sbievw ⊢ y z x ∈ z → φ ↔ x ∈ y → φ
6 5 albii ⊢ ∀ x y z x ∈ z → φ ↔ ∀ x x ∈ y → φ
7 elequ1 ⊢ x = y → x ∈ z ↔ y ∈ z
8 7 1 imbi12d ⊢ x = y → x ∈ z → φ ↔ y ∈ z → ψ
9 8 cbvalvw ⊢ ∀ x x ∈ z → φ ↔ ∀ y y ∈ z → ψ
10 df-ral ⊢ ∀ y ∈ x ψ ↔ ∀ y y ∈ x → ψ
11 10 sbbii ⊢ z x ∀ y ∈ x ψ ↔ z x ∀ y y ∈ x → ψ
12 sbal ⊢ z x ∀ y y ∈ x → ψ ↔ ∀ y z x y ∈ x → ψ
13 elequ2 ⊢ x = z → y ∈ x ↔ y ∈ z
14 13 imbi1d ⊢ x = z → y ∈ x → ψ ↔ y ∈ z → ψ
15 14 sbievw ⊢ z x y ∈ x → ψ ↔ y ∈ z → ψ
16 15 albii ⊢ ∀ y z x y ∈ x → ψ ↔ ∀ y y ∈ z → ψ
17 11 12 16 3bitrri ⊢ ∀ y y ∈ z → ψ ↔ z x ∀ y ∈ x ψ
18 9 17 bitri ⊢ ∀ x x ∈ z → φ ↔ z x ∀ y ∈ x ψ
19 18 sbbii ⊢ y z ∀ x x ∈ z → φ ↔ y z z x ∀ y ∈ x ψ
20 sbal ⊢ y z ∀ x x ∈ z → φ ↔ ∀ x y z x ∈ z → φ
21 sbco2vv ⊢ y z z x ∀ y ∈ x ψ ↔ y x ∀ y ∈ x ψ
22 19 20 21 3bitr3i ⊢ ∀ x y z x ∈ z → φ ↔ y x ∀ y ∈ x ψ
23 2 6 22 3bitr2i ⊢ ∀ x ∈ y φ ↔ y x ∀ y ∈ x ψ