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

Theorem r19.26 2676
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 445 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21ralimi 2619 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 449 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2619 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ps )
52, 4jca 520 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  -> 
( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
6 pm3.2 436 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
76ral2imi 2620 . . 3  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ( ph  /\  ps )
) )
87imp 420 . 2  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  A. x  e.  A  ( ph  /\ 
ps ) )
95, 8impbii 182 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 178    /\ wa 360   A.wral 2544
This theorem is referenced by:  r19.26-2  2677  r19.26-3  2678  ralbiim  2681  r19.27av  2682  r19.35  2688  reu8  2962  ssrab  3252  r19.28z  3547  r19.28zv  3550  r19.27z  3553  r19.27zv  3554  2ralunsn  3817  iuneq2  3922  disjxun  4022  asymref2  5059  cnvpo  5211  fncnv  5279  fnres  5325  fnopabg  5332  mpteqb  5575  eqfnfv3  5585  caoftrn  6073  abianfp  6466  iiner  6726  ixpeq2  6825  ixpin  6836  ixpfi2  7149  wemaplem2  7257  dfac5  7750  kmlem6  7776  eltsk2g  8368  intgru  8431  axgroth6  8445  fsequb  11031  rexanuz  11823  rexanre  11824  cau3lem  11832  rlimcn2  12058  o1of2  12080  o1rlimmul  12086  sqr2irr  12521  gcdcllem1  12684  pc11  12926  prmreclem2  12958  catpropd  13606  issubc3  13717  fucinv  13841  ispos2  14076  issubg3  14631  issubg4  14632  iunocv  16575  tgval2  16688  1stcelcls  17181  ptclsg  17303  ptcnplem  17309  fbun  17529  txflf  17695  prdsmet  17928  metequiv  18049  metequiv2  18050  iscau4  18699  cmetcaulem  18708  evthicc2  18814  ismbfcn  18980  mbfi1flimlem  19071  rolle  19331  itgsubst  19390  plydivex  19671  ulmcaulem  19765  ulmcau  19766  ulmbdd  19769  ulmcn  19770  mumullem2  20412  2sqlem6  20602  rngoueqz  21089  ocsh  21854  spanuni  22115  riesz4i  22635  leopadd  22704  leoptri  22708  leoptr  22709  dfpo2  23515  poseq  23654  wfr3g  23656  frr3g  23681  axpasch  23976  axeuclid  23998  axcontlem2  24000  axcontlem4  24002  axcontlem7  24005  r19.26-2a  24332  domintrefb  24461  celsor  24509  domintrefc  24524  svli2  24883  inttop2  24914  qusp  24941  tartarmap  25287  neibastop1  25707  inixp  25798  intidl  26053  mzpincl  26211  lerabdioph  26285  ltrabdioph  26288  nerabdioph  26289  dvdsrabdioph  26290  dford3lem1  26518  stoweidlem7  27155  stoweidlem54  27202  stoweidlem59  27207  2ralbiim  27331  2reu4a  27346  pclclN  29347  tendoeq2  30230
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549
This theorem depends on definitions:  df-bi 179  df-an 362  df-ral 2549
  Copyright terms: Public domain W3C validator