Theorem sbccomlem 3891

Description: Lemma for sbccom 3893. (Contributed by NM, 14-Nov-2005.) (Revised by Mario Carneiro, 18-Oct-2016.) Avoid ax-10 2141, 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 3814	. . 3 ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 → 𝐴 ∈ V)
2		sbcex 3814	. . . 4 ⊢ ([𝐵 / 𝑦][𝐴 / 𝑥]𝜑 → 𝐵 ∈ V)
3		sbc6g 3834	. . . . 5 ⊢ (𝐵 ∈ V → ([𝐵 / 𝑦][𝐴 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝐵 → [𝐴 / 𝑥]𝜑)))
4		isset 3502	. . . . . . 7 ⊢ (𝐵 ∈ V ↔ ∃𝑦 𝑦 = 𝐵)
5		exim 1832	. . . . . . 7 ⊢ (∀𝑦(𝑦 = 𝐵 → [𝐴 / 𝑥]𝜑) → (∃𝑦 𝑦 = 𝐵 → ∃𝑦[𝐴 / 𝑥]𝜑))
6	4, 5	biimtrid 242	. . . . . 6 ⊢ (∀𝑦(𝑦 = 𝐵 → [𝐴 / 𝑥]𝜑) → (𝐵 ∈ V → ∃𝑦[𝐴 / 𝑥]𝜑))
7		sbcex 3814	. . . . . . 7 ⊢ ([𝐴 / 𝑥]𝜑 → 𝐴 ∈ V)
8	7	exlimiv 1929	. . . . . 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 3834	. . . . 5 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → [𝐵 / 𝑦]𝜑)))
14		isset 3502	. . . . . . 7 ⊢ (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
15		exim 1832	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝐴 → [𝐵 / 𝑦]𝜑) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥[𝐵 / 𝑦]𝜑))
16	14, 15	biimtrid 242	. . . . . 6 ⊢ (∀𝑥(𝑥 = 𝐴 → [𝐵 / 𝑦]𝜑) → (𝐴 ∈ V → ∃𝑥[𝐵 / 𝑦]𝜑))
17		sbcex 3814	. . . . . . 7 ⊢ ([𝐵 / 𝑦]𝜑 → 𝐵 ∈ V)
18	17	exlimiv 1929	. . . . . 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 1818	. . . . . . 7 ⊢ (∀𝑥∀𝑦(𝑥 = 𝐴 → (𝑦 = 𝐵 → 𝜑)) ↔ ∀𝑥∀𝑦(𝑦 = 𝐵 → (𝑥 = 𝐴 → 𝜑)))
25		alcom 2160	. . . . . . 7 ⊢ (∀𝑥∀𝑦(𝑦 = 𝐵 → (𝑥 = 𝐴 → 𝜑)) ↔ ∀𝑦∀𝑥(𝑦 = 𝐵 → (𝑥 = 𝐴 → 𝜑)))
26	24, 25	bitri 275	. . . . . 6 ⊢ (∀𝑥∀𝑦(𝑥 = 𝐴 → (𝑦 = 𝐵 → 𝜑)) ↔ ∀𝑦∀𝑥(𝑦 = 𝐵 → (𝑥 = 𝐴 → 𝜑)))
27		19.21v 1938	. . . . . . 7 ⊢ (∀𝑦(𝑥 = 𝐴 → (𝑦 = 𝐵 → 𝜑)) ↔ (𝑥 = 𝐴 → ∀𝑦(𝑦 = 𝐵 → 𝜑)))
28	27	albii 1817	. . . . . 6 ⊢ (∀𝑥∀𝑦(𝑥 = 𝐴 → (𝑦 = 𝐵 → 𝜑)) ↔ ∀𝑥(𝑥 = 𝐴 → ∀𝑦(𝑦 = 𝐵 → 𝜑)))
29		19.21v 1938	. . . . . . 7 ⊢ (∀𝑥(𝑦 = 𝐵 → (𝑥 = 𝐴 → 𝜑)) ↔ (𝑦 = 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))
30	29	albii 1817	. . . . . 6 ⊢ (∀𝑦∀𝑥(𝑦 = 𝐵 → (𝑥 = 𝐴 → 𝜑)) ↔ ∀𝑦(𝑦 = 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))
31	26, 28, 30	3bitr3i 301	. . . . 5 ⊢ (∀𝑥(𝑥 = 𝐴 → ∀𝑦(𝑦 = 𝐵 → 𝜑)) ↔ ∀𝑦(𝑦 = 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝜑)))
32	31	a1i 11	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥(𝑥 = 𝐴 → ∀𝑦(𝑦 = 𝐵 → 𝜑)) ↔ ∀𝑦(𝑦 = 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
33		sbc6g 3834	. . . . . . 7 ⊢ (𝐵 ∈ V → ([𝐵 / 𝑦]𝜑 ↔ ∀𝑦(𝑦 = 𝐵 → 𝜑)))
34	33	imbi2d 340	. . . . . 6 ⊢ (𝐵 ∈ V → ((𝑥 = 𝐴 → [𝐵 / 𝑦]𝜑) ↔ (𝑥 = 𝐴 → ∀𝑦(𝑦 = 𝐵 → 𝜑))))
35	34	albidv 1919	. . . . 5 ⊢ (𝐵 ∈ V → (∀𝑥(𝑥 = 𝐴 → [𝐵 / 𝑦]𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → ∀𝑦(𝑦 = 𝐵 → 𝜑))))
36	35	adantl 481	. . . 4 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → (∀𝑥(𝑥 = 𝐴 → [𝐵 / 𝑦]𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → ∀𝑦(𝑦 = 𝐵 → 𝜑))))
37		sbc6g 3834	. . . . . . 7 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
38	37	imbi2d 340	. . . . . 6 ⊢ (𝐴 ∈ V → ((𝑦 = 𝐵 → [𝐴 / 𝑥]𝜑) ↔ (𝑦 = 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝜑))))
39	38	albidv 1919	. . . . 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 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488  [wsbc 3804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-11 2158  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-sbc 3805

This theorem is referenced by:  sbccom  3893