MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbc2or Structured version   Unicode version

Theorem sbc2or 3169
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 3185 (false) and sbc6 3187 (true) conclusions. This is interesting since dfsbcq 3163 and dfsbcq2 3164 (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.
StepHypRef Expression
1 dfsbcq2 3164 . . . 4  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
2 eqeq2 2445 . . . . . 6  |-  ( y  =  A  ->  (
x  =  y  <->  x  =  A ) )
32anbi1d 686 . . . . 5  |-  ( y  =  A  ->  (
( x  =  y  /\  ph )  <->  ( x  =  A  /\  ph )
) )
43exbidv 1636 . . . 4  |-  ( y  =  A  ->  ( E. x ( x  =  y  /\  ph )  <->  E. x ( x  =  A  /\  ph )
) )
5 sb5 2176 . . . 4  |-  ( [ y  /  x ] ph 
<->  E. x ( x  =  y  /\  ph ) )
61, 4, 5vtoclbg 3012 . . 3  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ph  <->  E. x ( x  =  A  /\  ph ) ) )
76orcd 382 . 2  |-  ( A  e.  _V  ->  (
( [. A  /  x ]. ph  <->  E. x ( x  =  A  /\  ph ) )  \/  ( [. A  /  x ]. ph  <->  A. x ( x  =  A  ->  ph )
) ) )
8 pm5.15 860 . . 3  |-  ( (
[. A  /  x ]. ph  <->  E. x ( x  =  A  /\  ph ) )  \/  ( [. A  /  x ]. ph  <->  -.  E. x
( x  =  A  /\  ph ) ) )
9 vex 2959 . . . . . . . . . 10  |-  x  e. 
_V
10 eleq1 2496 . . . . . . . . . 10  |-  ( x  =  A  ->  (
x  e.  _V  <->  A  e.  _V ) )
119, 10mpbii 203 . . . . . . . . 9  |-  ( x  =  A  ->  A  e.  _V )
1211adantr 452 . . . . . . . 8  |-  ( ( x  =  A  /\  ph )  ->  A  e.  _V )
1312con3i 129 . . . . . . 7  |-  ( -.  A  e.  _V  ->  -.  ( x  =  A  /\  ph ) )
1413nexdv 1941 . . . . . 6  |-  ( -.  A  e.  _V  ->  -. 
E. x ( x  =  A  /\  ph ) )
1511con3i 129 . . . . . . . 8  |-  ( -.  A  e.  _V  ->  -.  x  =  A )
1615pm2.21d 100 . . . . . . 7  |-  ( -.  A  e.  _V  ->  ( x  =  A  ->  ph ) )
1716alrimiv 1641 . . . . . 6  |-  ( -.  A  e.  _V  ->  A. x ( x  =  A  ->  ph ) )
1814, 172thd 232 . . . . 5  |-  ( -.  A  e.  _V  ->  ( -.  E. x ( x  =  A  /\  ph )  <->  A. x ( x  =  A  ->  ph )
) )
1918bibi2d 310 . . . 4  |-  ( -.  A  e.  _V  ->  ( ( [. A  /  x ]. ph  <->  -.  E. x
( x  =  A  /\  ph ) )  <-> 
( [. A  /  x ]. ph  <->  A. x ( x  =  A  ->  ph )
) ) )
2019orbi2d 683 . . 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 ) ) ) ) )
218, 20mpbii 203 . 2  |-  ( -.  A  e.  _V  ->  ( ( [. A  /  x ]. ph  <->  E. x
( x  =  A  /\  ph ) )  \/  ( [. A  /  x ]. ph  <->  A. x
( x  =  A  ->  ph ) ) ) )
227, 21pm2.61i 158 1  |-  ( (
[. A  /  x ]. ph  <->  E. x ( x  =  A  /\  ph ) )  \/  ( [. A  /  x ]. ph  <->  A. x ( x  =  A  ->  ph )
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359   A.wal 1549   E.wex 1550    = wceq 1652   [wsb 1658    e. wcel 1725   _Vcvv 2956   [.wsbc 3161
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-sbc 3162
  Copyright terms: Public domain W3C validator