Theorem sbc2or 3756

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 3775 (false) and sbc6 3778 (true) conclusions. This is interesting since dfsbcq 3749 and dfsbcq2 3750 (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 3750	. . . 4 ⊢ (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
2		eqeq2 2778	. . . . . 6 ⊢ (𝑦 = 𝐴 → (𝑥 = 𝑦 ↔ 𝑥 = 𝐴))
3	2	anbi1d 643	. . . . 5 ⊢ (𝑦 = 𝐴 → ((𝑥 = 𝑦 ∧ 𝜑) ↔ (𝑥 = 𝐴 ∧ 𝜑)))
4	3	exbidv 1954	. . . 4 ⊢ (𝑦 = 𝐴 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
5		sb5 2314	. . . 4 ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
6	1, 4, 5	vtoclbg 3527	. . 3 ⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
7	6	orcd 887	. 2 ⊢ (𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))))
8		pm5.15 1030	. . 3 ⊢ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)))
9		vex 3462	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
10		eleq1 2854	. . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ V ↔ 𝐴 ∈ V))
11	9, 10	mpbii 236	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → 𝐴 ∈ V)
12	11	adantr 486	. . . . . . . 8 ⊢ ((𝑥 = 𝐴 ∧ 𝜑) → 𝐴 ∈ V)
13	12	con3i 155	. . . . . . 7 ⊢ (¬ 𝐴 ∈ V → ¬ (𝑥 = 𝐴 ∧ 𝜑))
14	13	nexdv 1969	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))
15	11	con3i 155	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → ¬ 𝑥 = 𝐴)
16	15	pm2.21d 122	. . . . . . 7 ⊢ (¬ 𝐴 ∈ V → (𝑥 = 𝐴 → 𝜑))
17	16	alrimiv 1960	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → ∀𝑥(𝑥 = 𝐴 → 𝜑))
18	14, 17	2thd 268	. . . . 5 ⊢ (¬ 𝐴 ∈ V → (¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))
19	18	bibi2d 345	. . . 4 ⊢ (¬ 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ↔ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))))
20	19	orbi2d 929	. . 3 ⊢ (¬ 𝐴 ∈ V → ((([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑))) ↔ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))))
21	8, 20	mpbii 236	. 2 ⊢ (¬ 𝐴 ∈ V → (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑))))
22	7, 21	pm2.61i 184	1 ⊢ (([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) ∨ ([𝐴 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝐴 → 𝜑)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  ∀wal 1568   = wceq 1570  ∃wex 1812  [wsb 2099   ∈ wcel 2146  Vcvv 3458  [wsbc 3747

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-sbc 3748

This theorem is used by: (None)