Theorem sbc2or 3692

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 3711 (false) and sbc6 3715 (true) conclusions. This is interesting since dfsbcq 3685 and dfsbcq2 3686 (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 3686	. . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
2		eqeq2 2748	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐴))
3	2	anbi1d 633	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝐴 ∧ 𝜑)))
4	3	exbidv 1929	. . . 4 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
5		sb5 2274	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
6	1, 4, 5	vtoclbg 3473	. . 3 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
7	6	orcd 873	. 2 ⊢ (𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))))
8		pm5.15 1013	. . 3 ⊢ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
9		vex 3402	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
10		eleq1 2818	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
11	9, 10	mpbii 236	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)
12	11	adantr 484	. . . . . . . 8 ⊢ ((𝑥 = 𝐴 ∧ 𝜑) → 𝐴 ∈ V)
13	12	con3i 157	. . . . . . 7 ⊢ (¬ 𝐴 ∈ V → ¬ (𝑥 = 𝐴 ∧ 𝜑))
14	13	nexdv 1944	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
15	11	con3i 157	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → ¬ 𝑥 = 𝐴)
16	15	pm2.21d 121	. . . . . . 7 ⊢ (¬ 𝐴 ∈ V → (𝑥 = 𝐴 → 𝜑))
17	16	alrimiv 1935	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → ∀𝑥(𝑥 = 𝐴 → 𝜑))
18	14, 17	2thd 268	. . . . 5 ⊢ (¬ 𝐴 ∈ V → (¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
19	18	bibi2d 346	. . . 4 ⊢ (¬ 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ↔ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))))
20	19	orbi2d 916	. . 3 ⊢ (¬ 𝐴 ∈ V → ((([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) ↔ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))))
21	8, 20	mpbii 236	. 2 ⊢ (¬ 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))))
22	7, 21	pm2.61i 185	1 ⊢ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 847  ∀wal 1541   = wceq 1543  ∃wex 1787  [wsb 2072   ∈ wcel 2112  Vcvv 3398  [wsbc 3683

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-sbc 3684

This theorem is referenced by: (None)