Metamath Proof Explorer

Theorem dfich2

Description: Alternate definition of the property of a wff ph that the setvar variables x and y are interchangeable. (Contributed by AV and WL, 6-Aug-2023)

Ref Expression
Assertion dfich2 ⊢ x ⇄ y φ ↔ ∀ a ∀ b a x b y φ ↔ b x a y φ

Proof

Step Hyp Ref Expression
1 df-ich ⊢ x ⇄ y φ ↔ ∀ x ∀ y x z y x z y φ ↔ φ
2 nfs1v ⊢ Ⅎ y b y φ
3 2 nfsbv ⊢ Ⅎ y a x b y φ
4 3 nfsbv ⊢ Ⅎ y x b a x b y φ
5 nfv ⊢ Ⅎ a φ
6 4 5 sbbib ⊢ ∀ y y a x b a x b y φ ↔ φ ↔ ∀ a x b a x b y φ ↔ a y φ
7 6 albii ⊢ ∀ x ∀ y y a x b a x b y φ ↔ φ ↔ ∀ x ∀ a x b a x b y φ ↔ a y φ
8 sbco4 ⊢ y a x b a x b y φ ↔ x z y x z y φ
9 8 bibi1i ⊢ y a x b a x b y φ ↔ φ ↔ x z y x z y φ ↔ φ
10 9 2albii ⊢ ∀ x ∀ y y a x b a x b y φ ↔ φ ↔ ∀ x ∀ y x z y x z y φ ↔ φ
11 alcom ⊢ ∀ x ∀ a x b a x b y φ ↔ a y φ ↔ ∀ a ∀ x x b a x b y φ ↔ a y φ
12 nfs1v ⊢ Ⅎ x a x b y φ
13 nfv ⊢ Ⅎ b a y φ
14 12 13 sbbib ⊢ ∀ x x b a x b y φ ↔ a y φ ↔ ∀ b a x b y φ ↔ b x a y φ
15 14 albii ⊢ ∀ a ∀ x x b a x b y φ ↔ a y φ ↔ ∀ a ∀ b a x b y φ ↔ b x a y φ
16 11 15 bitri ⊢ ∀ x ∀ a x b a x b y φ ↔ a y φ ↔ ∀ a ∀ b a x b y φ ↔ b x a y φ
17 7 10 16 3bitr3i ⊢ ∀ x ∀ y x z y x z y φ ↔ φ ↔ ∀ a ∀ b a x b y φ ↔ b x a y φ
18 1 17 bitri ⊢ x ⇄ y φ ↔ ∀ a ∀ b a x b y φ ↔ b x a y φ