Theorem sbc2or 3055

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 [A / x]φ behavior at proper classes, matching the sbc5 3071 (false) and sbc6 3073 (true) conclusions. This is interesting since dfsbcq 3049 and dfsbcq2 3050 (from which it is derived) do not appear to say anything obvious about proper class behavior. Note that this theorem doesn't 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 y that φ or A may contain. (Contributed by NM, 11-Oct-2004.) (Proof modification is discouraged.)

Assertion

Ref	Expression
sbc2or	⊢ (([̣A / x]̣φ ↔ ∃x(x = A ∧ φ)) ∨ ([̣A / x]̣φ ↔ ∀x(x = A → φ)))

Distinct variable group:   x,A

Allowed substitution hint:   φ(x)

Proof of Theorem sbc2or

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq2 3050	. . . 4 ⊢ (y = A → ([y / x]φ ↔ [̣A / x]̣φ))
2		eqeq2 2362	. . . . . 6 ⊢ (y = A → (x = y ↔ x = A))
3	2	anbi1d 685	. . . . 5 ⊢ (y = A → ((x = y ∧ φ) ↔ (x = A ∧ φ)))
4	3	exbidv 1626	. . . 4 ⊢ (y = A → (∃x(x = y ∧ φ) ↔ ∃x(x = A ∧ φ)))
5		sb5 2100	. . . 4 ⊢ ([y / x]φ ↔ ∃x(x = y ∧ φ))
6	1, 4, 5	vtoclbg 2916	. . 3 ⊢ (A ∈ V → ([̣A / x]̣φ ↔ ∃x(x = A ∧ φ)))
7	6	orcd 381	. 2 ⊢ (A ∈ V → (([̣A / x]̣φ ↔ ∃x(x = A ∧ φ)) ∨ ([̣A / x]̣φ ↔ ∀x(x = A → φ))))
8		pm5.15 859	. . 3 ⊢ (([̣A / x]̣φ ↔ ∃x(x = A ∧ φ)) ∨ ([̣A / x]̣φ ↔ ¬ ∃x(x = A ∧ φ)))
9		vex 2863	. . . . . . . . . 10 ⊢ x ∈ V
10		eleq1 2413	. . . . . . . . . 10 ⊢ (x = A → (x ∈ V ↔ A ∈ V))
11	9, 10	mpbii 202	. . . . . . . . 9 ⊢ (x = A → A ∈ V)
12	11	adantr 451	. . . . . . . 8 ⊢ ((x = A ∧ φ) → A ∈ V)
13	12	con3i 127	. . . . . . 7 ⊢ (¬ A ∈ V → ¬ (x = A ∧ φ))
14	13	nexdv 1916	. . . . . 6 ⊢ (¬ A ∈ V → ¬ ∃x(x = A ∧ φ))
15	11	con3i 127	. . . . . . . 8 ⊢ (¬ A ∈ V → ¬ x = A)
16	15	pm2.21d 98	. . . . . . 7 ⊢ (¬ A ∈ V → (x = A → φ))
17	16	alrimiv 1631	. . . . . 6 ⊢ (¬ A ∈ V → ∀x(x = A → φ))
18	14, 17	2thd 231	. . . . 5 ⊢ (¬ A ∈ V → (¬ ∃x(x = A ∧ φ) ↔ ∀x(x = A → φ)))
19	18	bibi2d 309	. . . 4 ⊢ (¬ A ∈ V → (([̣A / x]̣φ ↔ ¬ ∃x(x = A ∧ φ)) ↔ ([̣A / x]̣φ ↔ ∀x(x = A → φ))))
20	19	orbi2d 682	. . 3 ⊢ (¬ A ∈ V → ((([̣A / x]̣φ ↔ ∃x(x = A ∧ φ)) ∨ ([̣A / x]̣φ ↔ ¬ ∃x(x = A ∧ φ))) ↔ (([̣A / x]̣φ ↔ ∃x(x = A ∧ φ)) ∨ ([̣A / x]̣φ ↔ ∀x(x = A → φ)))))
21	8, 20	mpbii 202	. 2 ⊢ (¬ A ∈ V → (([̣A / x]̣φ ↔ ∃x(x = A ∧ φ)) ∨ ([̣A / x]̣φ ↔ ∀x(x = A → φ))))
22	7, 21	pm2.61i 156	1 ⊢ (([̣A / x]̣φ ↔ ∃x(x = A ∧ φ)) ∨ ([̣A / x]̣φ ↔ ∀x(x = A → φ)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∨ wo 357   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642  [wsb 1648   ∈ wcel 1710  Vcvv 2860  [̣wsbc 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-sbc 3048

This theorem is referenced by: (None)