Metamath Proof Explorer

Theorem ichbi12i

Description: Equivalence for interchangeable setvar variables. (Contributed by AV, 29-Jul-2023)

Ref Expression
Hypothesis ichbi12i.1 ⊢ x = a ∧ y = b → ψ ↔ χ
Assertion ichbi12i ⊢ x ⇄ y ψ ↔ a ⇄ b χ

Proof

Step Hyp Ref Expression
1 ichbi12i.1 ⊢ x = a ∧ y = b → ψ ↔ χ
2 nfv ⊢ Ⅎ b ψ
3 2 sbco2v ⊢ v b b y ψ ↔ v y ψ
4 3 bicomi ⊢ v y ψ ↔ v b b y ψ
5 4 sbbii ⊢ a x v y ψ ↔ a x v b b y ψ
6 sbcom2 ⊢ a x v b b y ψ ↔ v b a x b y ψ
7 5 6 bitri ⊢ a x v y ψ ↔ v b a x b y ψ
8 7 sbbii ⊢ u a a x v y ψ ↔ u a v b a x b y ψ
9 nfv ⊢ Ⅎ a ψ
10 9 nfsbv ⊢ Ⅎ a v y ψ
11 10 sbco2v ⊢ u a a x v y ψ ↔ u x v y ψ
12 1 2sbievw ⊢ a x b y ψ ↔ χ
13 12 2sbbii ⊢ u a v b a x b y ψ ↔ u a v b χ
14 8 11 13 3bitr3i ⊢ u x v y ψ ↔ u a v b χ
15 sbcom2 ⊢ u b a x b y ψ ↔ a x u b b y ψ
16 2 sbco2v ⊢ u b b y ψ ↔ u y ψ
17 16 sbbii ⊢ a x u b b y ψ ↔ a x u y ψ
18 15 17 bitri ⊢ u b a x b y ψ ↔ a x u y ψ
19 18 sbbii ⊢ v a u b a x b y ψ ↔ v a a x u y ψ
20 12 2sbbii ⊢ v a u b a x b y ψ ↔ v a u b χ
21 9 nfsbv ⊢ Ⅎ a u y ψ
22 21 sbco2v ⊢ v a a x u y ψ ↔ v x u y ψ
23 19 20 22 3bitr3ri ⊢ v x u y ψ ↔ v a u b χ
24 14 23 bibi12i ⊢ u x v y ψ ↔ v x u y ψ ↔ u a v b χ ↔ v a u b χ
25 24 2albii ⊢ ∀ u ∀ v u x v y ψ ↔ v x u y ψ ↔ ∀ u ∀ v u a v b χ ↔ v a u b χ
26 dfich2 ⊢ x ⇄ y ψ ↔ ∀ u ∀ v u x v y ψ ↔ v x u y ψ
27 dfich2 ⊢ a ⇄ b χ ↔ ∀ u ∀ v u a v b χ ↔ v a u b χ
28 25 26 27 3bitr4i ⊢ x ⇄ y ψ ↔ a ⇄ b χ