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

Theorem sbc2or 3171
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 3187 (false) and sbc6 3189 (true) conclusions. This is interesting since dfsbcq 3165 and dfsbcq2 3166 (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 3166 . . . 4  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
2 eqeq2 2447 . . . . . 6  |-  ( y  =  A  ->  (
x  =  y  <->  x  =  A ) )
32anbi1d 687 . . . . 5  |-  ( y  =  A  ->  (
( x  =  y  /\  ph )  <->  ( x  =  A  /\  ph )
) )
43exbidv 1637 . . . 4  |-  ( y  =  A  ->  ( E. x ( x  =  y  /\  ph )  <->  E. x ( x  =  A  /\  ph )
) )
5 sb5 2178 . . . 4  |-  ( [ y  /  x ] ph 
<->  E. x ( x  =  y  /\  ph ) )
61, 4, 5vtoclbg 3014 . . 3  |-  ( A  e.  _V  ->  ( [. A  /  x ]. ph  <->  E. x ( x  =  A  /\  ph ) ) )
76orcd 383 . 2  |-  ( A  e.  _V  ->  (
( [. A  /  x ]. ph  <->  E. x ( x  =  A  /\  ph ) )  \/  ( [. A  /  x ]. ph  <->  A. x ( x  =  A  ->  ph )
) ) )
8 pm5.15 861 . . 3  |-  ( (
[. A  /  x ]. ph  <->  E. x ( x  =  A  /\  ph ) )  \/  ( [. A  /  x ]. ph  <->  -.  E. x
( x  =  A  /\  ph ) ) )
9 vex 2961 . . . . . . . . . 10  |-  x  e. 
_V
10 eleq1 2498 . . . . . . . . . 10  |-  ( x  =  A  ->  (
x  e.  _V  <->  A  e.  _V ) )
119, 10mpbii 204 . . . . . . . . 9  |-  ( x  =  A  ->  A  e.  _V )
1211adantr 453 . . . . . . . 8  |-  ( ( x  =  A  /\  ph )  ->  A  e.  _V )
1312con3i 130 . . . . . . 7  |-  ( -.  A  e.  _V  ->  -.  ( x  =  A  /\  ph ) )
1413nexdv 1942 . . . . . 6  |-  ( -.  A  e.  _V  ->  -. 
E. x ( x  =  A  /\  ph ) )
1511con3i 130 . . . . . . . 8  |-  ( -.  A  e.  _V  ->  -.  x  =  A )
1615pm2.21d 101 . . . . . . 7  |-  ( -.  A  e.  _V  ->  ( x  =  A  ->  ph ) )
1716alrimiv 1642 . . . . . 6  |-  ( -.  A  e.  _V  ->  A. x ( x  =  A  ->  ph ) )
1814, 172thd 233 . . . . 5  |-  ( -.  A  e.  _V  ->  ( -.  E. x ( x  =  A  /\  ph )  <->  A. x ( x  =  A  ->  ph )
) )
1918bibi2d 311 . . . 4  |-  ( -.  A  e.  _V  ->  ( ( [. A  /  x ]. ph  <->  -.  E. x
( x  =  A  /\  ph ) )  <-> 
( [. A  /  x ]. ph  <->  A. x ( x  =  A  ->  ph )
) ) )
2019orbi2d 684 . . 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 204 . 2  |-  ( -.  A  e.  _V  ->  ( ( [. A  /  x ]. ph  <->  E. x
( x  =  A  /\  ph ) )  \/  ( [. A  /  x ]. ph  <->  A. x
( x  =  A  ->  ph ) ) ) )
227, 21pm2.61i 159 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 178    \/ wo 359    /\ wa 360   A.wal 1550   E.wex 1551    = wceq 1653   [wsb 1659    e. wcel 1726   _Vcvv 2958   [.wsbc 3163
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-sbc 3164
  Copyright terms: Public domain W3C validator