Theorem sbc2or 3297

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 3313 (false) and sbc6 3315 (true) conclusions. This is interesting since dfsbcq 3290 and dfsbcq2 3291 (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 3291	. . . 4 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
2		eqeq2 2467	. . . . . 6 |- ( y = A -> ( x = y <-> x = A ) )
3	2	anbi1d 704	. . . . 5 |- ( y = A -> ( ( x = y /\ ph ) <-> ( x = A /\ ph ) ) )
4	3	exbidv 1681	. . . 4 |- ( y = A -> ( E. x ( x = y /\ ph ) <-> E. x ( x = A /\ ph ) ) )
5		sb5 2143	. . . 4 |- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )
6	1, 4, 5	vtoclbg 3131	. . 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 884	. . 3 |- ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> -. E. x ( x = A /\ ph ) ) )
9		vex 3075	. . . . . . . . . 10 |- x e. _V
10		eleq1 2524	. . . . . . . . . 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 1822	. . . . . 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 1686	. . . . . 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 1368   = wceq 1370   E.wex 1587   [wsb 1702   e. wcel 1758   _Vcvv 3072   [.wsbc 3288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794  ax-13 1954  ax-ext 2431

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-v 3074  df-sbc 3289

This theorem is referenced by: (None)