Theorem sbc2or 3336

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 3352 (false) and sbc6 3354 (true) conclusions. This is interesting since dfsbcq 3329 and dfsbcq2 3330 (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 3330	. . . 4 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
2		eqeq2 2472	. . . . . 6 |- ( y = A -> ( x = y <-> x = A ) )
3	2	anbi1d 704	. . . . 5 |- ( y = A -> ( ( x = y /\ ph ) <-> ( x = A /\ ph ) ) )
4	3	exbidv 1715	. . . 4 |- ( y = A -> ( E. x ( x = y /\ ph ) <-> E. x ( x = A /\ ph ) ) )
5		sb5 2175	. . . 4 |- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )
6	1, 4, 5	vtoclbg 3168	. . 3 |- ( A e. _V -> ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) )
7	6	orcd 392	. 2 |- ( A e. _V -> ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) ) )
8		pm5.15 889	. . 3 |- ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> -. E. x ( x = A /\ ph ) ) )
9		vex 3112	. . . . . . . . . 10 |- x e. _V
10		eleq1 2529	. . . . . . . . . 10 |- ( x = A -> ( x e. _V <-> A e. _V ) )
11	9, 10	mpbii 211	. . . . . . . . 9 |- ( x = A -> A e. _V )
12	11	adantr 465	. . . . . . . 8 |- ( ( x = A /\ ph ) -> A e. _V )
13	12	con3i 135	. . . . . . 7 |- ( -. A e. _V -> -. ( x = A /\ ph ) )
14	13	nexdv 1885	. . . . . 6 |- ( -. A e. _V -> -. E. x ( x = A /\ ph ) )
15	11	con3i 135	. . . . . . . 8 |- ( -. A e. _V -> -. x = A )
16	15	pm2.21d 106	. . . . . . 7 |- ( -. A e. _V -> ( x = A -> ph ) )
17	16	alrimiv 1720	. . . . . 6 |- ( -. A e. _V -> A. x ( x = A -> ph ) )
18	14, 17	2thd 240	. . . . 5 |- ( -. A e. _V -> ( -. E. x ( x = A /\ ph ) <-> A. x ( x = A -> ph ) ) )
19	18	bibi2d 318	. . . 4 |- ( -. A e. _V -> ( ( [. A / x ]. ph <-> -. E. x ( x = A /\ ph ) ) <-> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) ) )
20	19	orbi2d 701	. . 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 211	. 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 164	1 |- ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   A.wal 1393   = wceq 1395   E.wex 1613   [wsb 1740   e. wcel 1819   _Vcvv 3109   [.wsbc 3327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-sbc 3328

This theorem is referenced by: (None)