This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ichbi12i

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

Ref Expression
Hypothesis ichbi12i.1 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion ichbi12i ( [ 𝑥 ⇄ 𝑦 ] 𝜓 ↔ [ 𝑎 ⇄ 𝑏 ] 𝜒 )

Proof

Step Hyp Ref Expression
1 ichbi12i.1 ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝜓 ↔ 𝜒 ) )
2 nfv ⊢ Ⅎ 𝑏 𝜓
3 2 sbco2v ⊢ ( [ 𝑣 / 𝑏 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑦 ] 𝜓 )
4 3 bicomi ⊢ ( [ 𝑣 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑏 ] [ 𝑏 / 𝑦 ] 𝜓 )
5 4 sbbii ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] [ 𝑣 / 𝑏 ] [ 𝑏 / 𝑦 ] 𝜓 )
6 sbcom2 ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑣 / 𝑏 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 )
7 5 6 bitri ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 )
8 7 sbbii ⊢ ( [ 𝑢 / 𝑎 ] [ 𝑎 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ [ 𝑢 / 𝑎 ] [ 𝑣 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 )
9 nfv ⊢ Ⅎ 𝑎 𝜓
10 9 nfsbv ⊢ Ⅎ 𝑎 [ 𝑣 / 𝑦 ] 𝜓
11 10 sbco2v ⊢ ( [ 𝑢 / 𝑎 ] [ 𝑎 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 )
12 1 2sbievw ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ 𝜒 )
13 12 2sbbii ⊢ ( [ 𝑢 / 𝑎 ] [ 𝑣 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑢 / 𝑎 ] [ 𝑣 / 𝑏 ] 𝜒 )
14 8 11 13 3bitr3i ⊢ ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ [ 𝑢 / 𝑎 ] [ 𝑣 / 𝑏 ] 𝜒 )
15 sbcom2 ⊢ ( [ 𝑢 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑏 ] [ 𝑏 / 𝑦 ] 𝜓 )
16 2 sbco2v ⊢ ( [ 𝑢 / 𝑏 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑢 / 𝑦 ] 𝜓 )
17 16 sbbii ⊢ ( [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑏 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 )
18 15 17 bitri ⊢ ( [ 𝑢 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 )
19 18 sbbii ⊢ ( [ 𝑣 / 𝑎 ] [ 𝑢 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑎 ] [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 )
20 12 2sbbii ⊢ ( [ 𝑣 / 𝑎 ] [ 𝑢 / 𝑏 ] [ 𝑎 / 𝑥 ] [ 𝑏 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜒 )
21 9 nfsbv ⊢ Ⅎ 𝑎 [ 𝑢 / 𝑦 ] 𝜓
22 21 sbco2v ⊢ ( [ 𝑣 / 𝑎 ] [ 𝑎 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 )
23 19 20 22 3bitr3ri ⊢ ( [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜒 )
24 14 23 bibi12i ⊢ ( ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) ↔ ( [ 𝑢 / 𝑎 ] [ 𝑣 / 𝑏 ] 𝜒 ↔ [ 𝑣 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜒 ) )
25 24 2albii ⊢ ( ∀ 𝑢 ∀ 𝑣 ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) ↔ ∀ 𝑢 ∀ 𝑣 ( [ 𝑢 / 𝑎 ] [ 𝑣 / 𝑏 ] 𝜒 ↔ [ 𝑣 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜒 ) )
26 dfich2 ⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜓 ↔ ∀ 𝑢 ∀ 𝑣 ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜓 ↔ [ 𝑣 / 𝑥 ] [ 𝑢 / 𝑦 ] 𝜓 ) )
27 dfich2 ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜒 ↔ ∀ 𝑢 ∀ 𝑣 ( [ 𝑢 / 𝑎 ] [ 𝑣 / 𝑏 ] 𝜒 ↔ [ 𝑣 / 𝑎 ] [ 𝑢 / 𝑏 ] 𝜒 ) )
28 25 26 27 3bitr4i ⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜓 ↔ [ 𝑎 ⇄ 𝑏 ] 𝜒 )