Theorem sbc2or 3192

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 3208 (false) and sbc6 3210 (true) conclusions. This is interesting since dfsbcq 3185 and dfsbcq2 3186 (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 3186	. . . 4 |- ( y = A -> ( [ y / x ] ph <-> [. A / x ]. ph ) )
2		eqeq2 2450	. . . . . 6 |- ( y = A -> ( x = y <-> x = A ) )
3	2	anbi1d 699	. . . . 5 |- ( y = A -> ( ( x = y /\ ph ) <-> ( x = A /\ ph ) ) )
4	3	exbidv 1685	. . . 4 |- ( y = A -> ( E. x ( x = y /\ ph ) <-> E. x ( x = A /\ ph ) ) )
5		sb5 2140	. . . 4 |- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )
6	1, 4, 5	vtoclbg 3028	. . 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 879	. . 3 |- ( ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) \/ ( [. A / x ]. ph <-> -. E. x ( x = A /\ ph ) ) )
9		vex 2973	. . . . . . . . . 10 |- x e. _V
10		eleq1 2501	. . . . . . . . . 10 |- ( x = A -> ( x e. _V <-> A e. _V ) )
11	9, 10	mpbii 211	. . . . . . . . 9 |- ( x = A -> A e. _V )
12	11	adantr 462	. . . . . . . 8 |- ( ( x = A /\ ph ) -> A e. _V )
13	12	con3i 135	. . . . . . 7 |- ( -. A e. _V -> -. ( x = A /\ ph ) )
14	13	nexdv 1939	. . . . . 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 1690	. . . . . 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 696	. . 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 1362   = wceq 1364   E.wex 1591   [wsb 1705   e. wcel 1761   _Vcvv 2970   [.wsbc 3183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-v 2972  df-sbc 3184

This theorem is referenced by: (None)