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

Theorem r19.26 2830
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 2773 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 448 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2773 . . 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 2774 . . 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 2697
This theorem is referenced by:  r19.26-2  2831  r19.26-3  2832  ralbiim  2835  r19.27av  2836  r19.35  2847  reu8  3122  ssrab  3413  r19.28z  3712  r19.28zv  3715  r19.27z  3718  r19.27zv  3719  2ralunsn  3996  iuneq2  4101  disjxun  4202  asymref2  5243  cnvpo  5402  fncnv  5507  fnres  5553  fnopabg  5560  mpteqb  5811  eqfnfv3  5821  caoftrn  6331  abianfp  6708  iiner  6968  ixpeq2  7068  ixpin  7079  ixpfi2  7397  wemaplem2  7506  dfac5  7999  kmlem6  8025  eltsk2g  8616  intgru  8679  axgroth6  8693  fsequb  11304  rexanuz  12139  rexanre  12140  cau3lem  12148  rlimcn2  12374  o1of2  12396  o1rlimmul  12402  climbdd  12455  sqr2irr  12838  gcdcllem1  13001  pc11  13243  prmreclem2  13275  catpropd  13925  issubc3  14036  fucinv  14160  ispos2  14395  issubg3  14950  issubg4  14951  iunocv  16898  tgval2  17011  1stcelcls  17514  ptclsg  17637  ptcnplem  17643  fbun  17862  txflf  18028  ucncn  18305  prdsmet  18390  metequiv  18529  metequiv2  18530  iscau4  19222  cmetcaulem  19231  evthicc2  19347  ismbfcn  19513  mbfi1flimlem  19604  rolle  19864  itgsubst  19923  plydivex  20204  ulmcaulem  20300  ulmcau  20301  ulmbdd  20304  ulmcn  20305  mumullem2  20953  2sqlem6  21143  rngoueqz  22008  ocsh  22775  spanuni  23036  riesz4i  23556  leopadd  23625  leoptri  23629  leoptr  23630  mptfnf  24063  voliune  24575  volfiniune  24576  dfpo2  25368  poseq  25513  wfr3g  25522  frr3g  25546  axpasch  25845  axeuclid  25867  axcontlem2  25869  axcontlem4  25871  axcontlem7  25874  ovoliunnfl  26211  voliunnfl  26213  volsupnfl  26214  itg2addnc  26222  neibastop1  26342  inixp  26384  intidl  26593  mzpincl  26745  lerabdioph  26819  ltrabdioph  26822  nerabdioph  26823  dvdsrabdioph  26824  dford3lem1  27051  stoweidlem7  27687  stoweidlem54  27734  2ralbiim  27883  2reu4a  27898  usgfiregdegfi  28278  usgreghash2spot  28359  pclclN  30589  tendoeq2  31472
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ral 2702
  Copyright terms: Public domain W3C validator