Theorem sbccomlem 3849

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

Assertion

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

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem sbccomlem

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3464  [wsbc 3770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-11 2158  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-sbc 3771

This theorem is referenced by:  sbccom  3851