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

Theorem r19.26 2781
Description: Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (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 444 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21ralimi 2724 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 448 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2724 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ps )
52, 4jca 519 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  -> 
( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
6 pm3.2 435 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
76ral2imi 2725 . . 3  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ( ph  /\  ps )
) )
87imp 419 . 2  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  A. x  e.  A  ( ph  /\ 
ps ) )
95, 8impbii 181 1  |-  ( A. x  e.  A  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   A.wral 2649
This theorem is referenced by:  r19.26-2  2782  r19.26-3  2783  ralbiim  2786  r19.27av  2787  r19.35  2798  reu8  3073  ssrab  3364  r19.28z  3663  r19.28zv  3666  r19.27z  3669  r19.27zv  3670  2ralunsn  3946  iuneq2  4051  disjxun  4151  asymref2  5191  cnvpo  5350  fncnv  5455  fnres  5501  fnopabg  5508  mpteqb  5758  eqfnfv3  5768  caoftrn  6278  abianfp  6652  iiner  6912  ixpeq2  7012  ixpin  7023  ixpfi2  7340  wemaplem2  7449  dfac5  7942  kmlem6  7968  eltsk2g  8559  intgru  8622  axgroth6  8636  fsequb  11241  rexanuz  12076  rexanre  12077  cau3lem  12085  rlimcn2  12311  o1of2  12333  o1rlimmul  12339  climbdd  12392  sqr2irr  12775  gcdcllem1  12938  pc11  13180  prmreclem2  13212  catpropd  13862  issubc3  13973  fucinv  14097  ispos2  14332  issubg3  14887  issubg4  14888  iunocv  16831  tgval2  16944  1stcelcls  17445  ptclsg  17568  ptcnplem  17574  fbun  17793  txflf  17959  ucncn  18236  prdsmet  18308  metequiv  18429  metequiv2  18430  iscau4  19103  cmetcaulem  19112  evthicc2  19224  ismbfcn  19390  mbfi1flimlem  19481  rolle  19741  itgsubst  19800  plydivex  20081  ulmcaulem  20177  ulmcau  20178  ulmbdd  20181  ulmcn  20182  mumullem2  20830  2sqlem6  21020  rngoueqz  21866  ocsh  22633  spanuni  22894  riesz4i  23414  leopadd  23483  leoptri  23487  leoptr  23488  mptfnf  23915  voliune  24379  volfiniune  24380  dfpo2  25136  poseq  25277  wfr3g  25279  frr3g  25304  axpasch  25594  axeuclid  25616  axcontlem2  25618  axcontlem4  25620  axcontlem7  25623  ovoliunnfl  25953  voliunnfl  25955  volsupnfl  25956  itg2addnc  25959  neibastop1  26079  inixp  26121  intidl  26330  mzpincl  26482  lerabdioph  26556  ltrabdioph  26559  nerabdioph  26560  dvdsrabdioph  26561  dford3lem1  26788  stoweidlem7  27424  stoweidlem54  27471  2ralbiim  27620  2reu4a  27635  pclclN  30005  tendoeq2  30888
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ral 2654
  Copyright terms: Public domain W3C validator