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

Metamath Proof Explorer

Theorem sbccomlem

Description: Lemma for sbccom . (Contributed by NM, 14-Nov-2005) (Revised by Mario Carneiro, 18-Oct-2016) Avoid ax-10 , ax-12 . (Revised by SN, 20-Aug-2025)

Ref Expression
Assertion sbccomlem ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 sbcex ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 → 𝐴 ∈ V )
2 sbcex ⊢ ( [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 → 𝐵 ∈ V )
3 sbc6g ⊢ ( 𝐵 ∈ V → ( [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → [ 𝐴 / 𝑥 ] 𝜑 ) ) )
4 isset ⊢ ( 𝐵 ∈ V ↔ ∃ 𝑦 𝑦 = 𝐵 )
5 exim ⊢ ( ∀ 𝑦 ( 𝑦 = 𝐵 → [ 𝐴 / 𝑥 ] 𝜑 ) → ( ∃ 𝑦 𝑦 = 𝐵 → ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) )
6 4 5 biimtrid ⊢ ( ∀ 𝑦 ( 𝑦 = 𝐵 → [ 𝐴 / 𝑥 ] 𝜑 ) → ( 𝐵 ∈ V → ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 ) )
7 sbcex ⊢ ( [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
8 7 exlimiv ⊢ ( ∃ 𝑦 [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
9 6 8 syl6com ⊢ ( 𝐵 ∈ V → ( ∀ 𝑦 ( 𝑦 = 𝐵 → [ 𝐴 / 𝑥 ] 𝜑 ) → 𝐴 ∈ V ) )
10 3 9 sylbid ⊢ ( 𝐵 ∈ V → ( [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V ) )
11 2 10 mpcom ⊢ ( [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 → 𝐴 ∈ V )
12 1 11 pm5.21ni ⊢ ( ¬ 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ) )
13 sbc6g ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → [ 𝐵 / 𝑦 ] 𝜑 ) ) )
14 isset ⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
15 exim ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → [ 𝐵 / 𝑦 ] 𝜑 ) → ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 [ 𝐵 / 𝑦 ] 𝜑 ) )
16 14 15 biimtrid ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → [ 𝐵 / 𝑦 ] 𝜑 ) → ( 𝐴 ∈ V → ∃ 𝑥 [ 𝐵 / 𝑦 ] 𝜑 ) )
17 sbcex ⊢ ( [ 𝐵 / 𝑦 ] 𝜑 → 𝐵 ∈ V )
18 17 exlimiv ⊢ ( ∃ 𝑥 [ 𝐵 / 𝑦 ] 𝜑 → 𝐵 ∈ V )
19 16 18 syl6com ⊢ ( 𝐴 ∈ V → ( ∀ 𝑥 ( 𝑥 = 𝐴 → [ 𝐵 / 𝑦 ] 𝜑 ) → 𝐵 ∈ V ) )
20 13 19 sylbid ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 → 𝐵 ∈ V ) )
21 1 20 mpcom ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 → 𝐵 ∈ V )
22 21 2 pm5.21ni ⊢ ( ¬ 𝐵 ∈ V → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ) )
23 bi2.04 ⊢ ( ( 𝑥 = 𝐴 → ( 𝑦 = 𝐵 → 𝜑 ) ) ↔ ( 𝑦 = 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
24 23 2albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝑦 = 𝐵 → 𝜑 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
25 alcom ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
26 24 25 bitri ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝑦 = 𝐵 → 𝜑 ) ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) )
27 19.21v ⊢ ( ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝑦 = 𝐵 → 𝜑 ) ) ↔ ( 𝑥 = 𝐴 → ∀ 𝑦 ( 𝑦 = 𝐵 → 𝜑 ) ) )
28 27 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝐴 → ( 𝑦 = 𝐵 → 𝜑 ) ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → ∀ 𝑦 ( 𝑦 = 𝐵 → 𝜑 ) ) )
29 19.21v ⊢ ( ∀ 𝑥 ( 𝑦 = 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) ↔ ( 𝑦 = 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
30 29 albii ⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝐵 → ( 𝑥 = 𝐴 → 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
31 26 28 30 3bitr3i ⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ∀ 𝑦 ( 𝑦 = 𝐵 → 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
32 31 a1i ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → ∀ 𝑦 ( 𝑦 = 𝐵 → 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) )
33 sbc6g ⊢ ( 𝐵 ∈ V → ( [ 𝐵 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → 𝜑 ) ) )
34 33 imbi2d ⊢ ( 𝐵 ∈ V → ( ( 𝑥 = 𝐴 → [ 𝐵 / 𝑦 ] 𝜑 ) ↔ ( 𝑥 = 𝐴 → ∀ 𝑦 ( 𝑦 = 𝐵 → 𝜑 ) ) ) )
35 34 albidv ⊢ ( 𝐵 ∈ V → ( ∀ 𝑥 ( 𝑥 = 𝐴 → [ 𝐵 / 𝑦 ] 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → ∀ 𝑦 ( 𝑦 = 𝐵 → 𝜑 ) ) ) )
36 35 adantl ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → [ 𝐵 / 𝑦 ] 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → ∀ 𝑦 ( 𝑦 = 𝐵 → 𝜑 ) ) ) )
37 sbc6g ⊢ ( 𝐴 ∈ V → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) )
38 37 imbi2d ⊢ ( 𝐴 ∈ V → ( ( 𝑦 = 𝐵 → [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ( 𝑦 = 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) )
39 38 albidv ⊢ ( 𝐴 ∈ V → ( ∀ 𝑦 ( 𝑦 = 𝐵 → [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) )
40 39 adantr ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ∀ 𝑦 ( 𝑦 = 𝐵 → [ 𝐴 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → ∀ 𝑥 ( 𝑥 = 𝐴 → 𝜑 ) ) ) )
41 32 36 40 3bitr4d ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ∀ 𝑥 ( 𝑥 = 𝐴 → [ 𝐵 / 𝑦 ] 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → [ 𝐴 / 𝑥 ] 𝜑 ) ) )
42 13 adantr ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝐴 → [ 𝐵 / 𝑦 ] 𝜑 ) ) )
43 3 adantl ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝐵 → [ 𝐴 / 𝑥 ] 𝜑 ) ) )
44 41 42 43 3bitr4d ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 ) )
45 12 22 44 ecase ⊢ ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑 ↔ [ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )