Theorem sbc2or 3749

Description: The disjunction of two equivalences for class substitution does not require a class existence hypothesis. This theorem tells us that there are only 2 possibilities for [𝐴 / 𝑥]𝜑 behavior at proper classes, matching the sbc5 3768 (false) and sbc6 3771 (true) conclusions. This is interesting since dfsbcq 3742 and dfsbcq2 3743 (from which it is derived) do not appear to say anything obvious about proper class behavior. Note that this theorem does not tell us that it is always one or the other at proper classes; it could "flip" between false (the first disjunct) and true (the second disjunct) as a function of some other variable 𝑦 that 𝜑 or 𝐴 may contain. (Contributed by NM, 11-Oct-2004.) (Proof modification is discouraged.)

Assertion

Ref	Expression
sbc2or	⊢ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem sbc2or

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq2 3743	. . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
2		eqeq2 2748	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐴))
3	2	anbi1d 631	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝐴 ∧ 𝜑)))
4	3	exbidv 1922	. . . 4 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
5		sb5 2282	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
6	1, 4, 5	vtoclbg 3514	. . 3 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
7	6	orcd 873	. 2 ⊢ (𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))))
8		pm5.15 1014	. . 3 ⊢ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
9		vex 3444	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
10		eleq1 2824	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
11	9, 10	mpbii 233	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)
12	11	adantr 480	. . . . . . . 8 ⊢ ((𝑥 = 𝐴 ∧ 𝜑) → 𝐴 ∈ V)
13	12	con3i 154	. . . . . . 7 ⊢ (¬ 𝐴 ∈ V → ¬ (𝑥 = 𝐴 ∧ 𝜑))
14	13	nexdv 1937	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
15	11	con3i 154	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → ¬ 𝑥 = 𝐴)
16	15	pm2.21d 121	. . . . . . 7 ⊢ (¬ 𝐴 ∈ V → (𝑥 = 𝐴 → 𝜑))
17	16	alrimiv 1928	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → ∀𝑥(𝑥 = 𝐴 → 𝜑))
18	14, 17	2thd 265	. . . . 5 ⊢ (¬ 𝐴 ∈ V → (¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
19	18	bibi2d 342	. . . 4 ⊢ (¬ 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ↔ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))))
20	19	orbi2d 915	. . 3 ⊢ (¬ 𝐴 ∈ V → ((([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) ↔ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))))
21	8, 20	mpbii 233	. 2 ⊢ (¬ 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))))
22	7, 21	pm2.61i 182	1 ⊢ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847  ∀wal 1539   = wceq 1541  ∃wex 1780  [wsb 2067   ∈ wcel 2113  Vcvv 3440  [wsbc 3740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-sbc 3741

This theorem is referenced by: (None)