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

Theorem r19.26 2929
Description: Restricted quantifier version of 19.26 1743. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.26  |-  ( A. x  e.  A  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )

Proof of Theorem r19.26
StepHypRef Expression
1 simpl 463 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21ralimi 2793 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 467 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2793 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ps )
52, 4jca 539 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  -> 
( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
6 pm3.2 453 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
76ral2imi 2788 . . 3  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ( ph  /\  ps )
) )
87imp 435 . 2  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  A. x  e.  A  ( ph  /\ 
ps ) )
95, 8impbii 192 1  |-  ( A. x  e.  A  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693
This theorem depends on definitions:  df-bi 190  df-an 377  df-ral 2754
This theorem is referenced by:  r19.26-2  2930  r19.26-3  2931  ralbiim  2934  r19.27v  2935  r19.35  2949  reu8  3246  ssrab  3519  r19.28z  3873  r19.28zv  3876  r19.27z  3880  r19.27zv  3881  2ralunsn  4201  iuneq2  4309  disjxun  4414  asymref2  5236  cnvpo  5393  fncnv  5669  fnres  5714  mptfnf  5721  fnopabg  5723  mpteqb  5987  eqfnfv3  6001  fvn0ssdmfun  6036  caoftrn  6593  wfr3g  7060  iiner  7461  ixpeq2  7562  ixpin  7573  ixpfi2  7898  wemaplem2  8088  dfac5  8585  kmlem6  8611  eltsk2g  9202  intgru  9265  axgroth6  9279  fsequb  12220  rexanuz  13457  rexanre  13458  cau3lem  13466  rlimcn2  13703  o1of2  13725  o1rlimmul  13731  climbdd  13784  sqrt2irr  14350  gcdcllem1  14522  pc11  14878  prmreclem2  14910  catpropd  15663  issubc3  15803  fucinv  15927  ispos2  16242  issubg3  16884  issubg4  16885  pmtrdifwrdel2  17176  ringsrg  17868  cply1mul  18936  iunocv  19293  scmatf1  19605  cpmatsubgpmat  19793  tgval2  20020  1stcelcls  20525  ptclsg  20679  ptcnplem  20685  fbun  20904  txflf  21070  ucncn  21349  prdsmet  21434  metequiv  21573  metequiv2  21574  iscau4  22298  cmetcaulem  22307  evthicc2  22460  ismbfcn  22636  mbfi1flimlem  22729  rolle  22991  itgsubst  23050  plydivex  23299  ulmcaulem  23398  ulmcau  23399  ulmbdd  23402  ulmcn  23403  mumullem2  24156  2sqlem6  24346  tgcgr4  24625  axpasch  25020  axeuclid  25042  axcontlem2  25044  axcontlem4  25046  axcontlem7  25049  usg2wlkeq  25485  usgfiregdegfi  25688  usgreghash2spot  25846  frgrareg  25894  frgraregord013  25895  friendshipgt3  25898  rngoueqz  26207  ocsh  26985  spanuni  27246  riesz4i  27765  leopadd  27834  leoptri  27838  leoptr  27839  disjunsn  28253  voliune  29101  volfiniune  29102  eulerpartlemr  29256  eulerpartlemn  29263  dfpo2  30444  poseq  30540  wzel  30556  frr3g  30562  neibastop1  31064  phpreu  31974  ptrecube  31985  poimirlem23  32008  poimirlem27  32012  ovoliunnfl  32027  voliunnfl  32029  volsupnfl  32030  itg2addnc  32041  inixp  32100  intidl  32307  pclclN  33501  tendoeq2  34386  mzpincl  35621  lerabdioph  35693  ltrabdioph  35696  nerabdioph  35697  dvdsrabdioph  35698  dford3lem1  35926  stoweidlem7  37905  stoweidlem54  37953  dirkercncflem3  38005  2ralbiim  38633  2reu4a  38648  ralnralall  39025  uhgrvd0nedgb  39595  fusgrregdegfi  39636  rusgr1vtxlem  39652  lfgriswlk  39723  1wlkdlem4  39728  ply1mulgsumlem1  40451  ldepsnlinclem1  40571  ldepsnlinclem2  40572
  Copyright terms: Public domain W3C validator