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

Theorem r19.26 2955
Description: Restricted quantifier version of 19.26 1725. (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 458 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21ralimi 2818 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 462 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2818 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ps )
52, 4jca 534 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  -> 
( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
6 pm3.2 448 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
76ral2imi 2813 . . 3  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ( ph  /\  ps )
) )
87imp 430 . 2  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  A. x  e.  A  ( ph  /\ 
ps ) )
95, 8impbii 190 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 187    /\ wa 370   A.wral 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2780
This theorem is referenced by:  r19.26-2  2956  r19.26-3  2957  ralbiim  2960  r19.27v  2961  r19.35  2975  reu8  3267  ssrab  3539  r19.28z  3889  r19.28zv  3892  r19.27z  3896  r19.27zv  3897  2ralunsn  4205  iuneq2  4313  disjxun  4418  asymref2  5232  cnvpo  5389  fncnv  5661  fnres  5706  mptfnf  5713  fnopabg  5715  mpteqb  5976  eqfnfv3  5989  fvn0ssdmfun  6024  caoftrn  6576  wfr3g  7038  iiner  7439  ixpeq2  7540  ixpin  7551  ixpfi2  7874  wemaplem2  8064  dfac5  8559  kmlem6  8585  eltsk2g  9176  intgru  9239  axgroth6  9253  fsequb  12187  rexanuz  13396  rexanre  13397  cau3lem  13405  rlimcn2  13641  o1of2  13663  o1rlimmul  13669  climbdd  13722  sqrt2irr  14288  gcdcllem1  14460  pc11  14816  prmreclem2  14848  catpropd  15601  issubc3  15741  fucinv  15865  ispos2  16180  issubg3  16822  issubg4  16823  pmtrdifwrdel2  17114  ringsrg  17806  cply1mul  18874  iunocv  19230  scmatf1  19542  cpmatsubgpmat  19730  tgval2  19957  1stcelcls  20462  ptclsg  20616  ptcnplem  20622  fbun  20841  txflf  21007  ucncn  21286  prdsmet  21371  metequiv  21510  metequiv2  21511  iscau4  22235  cmetcaulem  22244  evthicc2  22397  ismbfcn  22573  mbfi1flimlem  22666  rolle  22928  itgsubst  22987  plydivex  23236  ulmcaulem  23335  ulmcau  23336  ulmbdd  23339  ulmcn  23340  mumullem2  24093  2sqlem6  24283  tgcgr4  24562  axpasch  24957  axeuclid  24979  axcontlem2  24981  axcontlem4  24983  axcontlem7  24986  usg2wlkeq  25421  usgfiregdegfi  25624  usgreghash2spot  25782  frgrareg  25830  frgraregord013  25831  friendshipgt3  25834  rngoueqz  26143  ocsh  26921  spanuni  27182  riesz4i  27701  leopadd  27770  leoptri  27774  leoptr  27775  disjunsn  28193  voliune  29047  volfiniune  29048  eulerpartlemr  29202  eulerpartlemn  29209  dfpo2  30389  poseq  30485  wzel  30501  frr3g  30507  neibastop1  31007  phpreu  31842  ptrecube  31853  poimirlem23  31876  poimirlem27  31880  ovoliunnfl  31895  voliunnfl  31897  volsupnfl  31898  itg2addnc  31909  inixp  31968  intidl  32175  pclclN  33374  tendoeq2  34259  mzpincl  35494  lerabdioph  35566  ltrabdioph  35569  nerabdioph  35570  dvdsrabdioph  35571  dford3lem1  35800  stoweidlem7  37686  stoweidlem54  37734  dirkercncflem3  37786  2ralbiim  38307  2reu4a  38322  ralnralall  38692  ply1mulgsumlem1  39451  ldepsnlinclem1  39571  ldepsnlinclem2  39572
  Copyright terms: Public domain W3C validator