Theorem sbc2or 3244

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 ] ph behavior at proper classes, matching the sbc5 3260 (false) and sbc6 3262 (true) conclusions. This is interesting since dfsbcq 3237 and dfsbcq2 3238 (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 ph or A may contain. (Contributed by NM, 11-Oct-2004.) (Proof modification is discouraged.)

Assertion

Ref	Expression
sbc2or	|- ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )

Distinct variable group:   x, A

Allowed substitution hint:   ph( x)

Proof of Theorem sbc2or

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsbcq2 3238	. . . 4 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
2		eqeq2 2463	. . . . . 6 |- ( y = A -> ( x = y <-> x = A ) )
3	2	anbi1d 716	. . . . 5 |- ( y = A -> ( ( x = y /\ ph ) <-> ( x = A /\ ph ) ) )
4	3	exbidv 1772	. . . 4 |- ( y = A -> ( E. x ( x = y /\ ph ) <-> E. x ( x = A /\ ph ) ) )
5		sb5 2260	. . . 4 |- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )
6	1, 4, 5	vtoclbg 3076	. . 3 |- ( A e. _V -> ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) )
7	6	orcd 398	. 2 |- ( A e. _V -> ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) ) )
8		pm5.15 903	. . 3 |- ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> -. E. x ( x = A /\ ph ) ) )
9		vex 3016	. . . . . . . . . 10 |- x e. _V
10		eleq1 2518	. . . . . . . . . 10 |- ( x = A -> ( x e. _V <-> A e. _V ) )
11	9, 10	mpbii 216	. . . . . . . . 9 |- ( x = A -> A e. _V )
12	11	adantr 471	. . . . . . . 8 |- ( ( x = A /\ ph ) -> A e. _V )
13	12	con3i 142	. . . . . . 7 |- ( -. A e. _V -> -. ( x = A /\ ph ) )
14	13	nexdv 1786	. . . . . 6 |- ( -. A e. _V -> -. E. x ( x = A /\ ph ) )
15	11	con3i 142	. . . . . . . 8 |- ( -. A e. _V -> -. x = A )
16	15	pm2.21d 110	. . . . . . 7 |- ( -. A e. _V -> ( x = A -> ph ) )
17	16	alrimiv 1777	. . . . . 6 |- ( -. A e. _V -> A. x ( x = A -> ph ) )
18	14, 17	2thd 248	. . . . 5 |- ( -. A e. _V -> ( -. E. x ( x = A /\ ph ) <-> A. x ( x = A -> ph ) ) )
19	18	bibi2d 324	. . . 4 |- ( -. A e. _V -> ( ( [. A / x ]. ph <-> -. E. x ( x = A /\ ph ) ) <-> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) ) )
20	19	orbi2d 713	. . 3 |- ( -. A e. _V -> ( ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> -. E. x ( x = A /\ ph ) ) ) <-> ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) ) ) )
21	8, 20	mpbii 216	. 2 |- ( -. A e. _V -> ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) ) )
22	7, 21	pm2.61i 169	1 |- ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   \/ wo 374   /\ wa 375   A.wal 1446   = wceq 1448   E.wex 1667   [wsb 1801   e. wcel 1891   _Vcvv 3013   [.wsbc 3235

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-v 3015  df-sbc 3236

This theorem is referenced by: (None)