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

Theorem r19.26 2839
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 454 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21ralimi 2781 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 458 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2781 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ps )
52, 4jca 529 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  -> 
( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
6 pm3.2 445 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
76ral2imi 2782 . . 3  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ( ph  /\  ps )
) )
87imp 429 . 2  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  A. x  e.  A  ( ph  /\ 
ps ) )
95, 8impbii 188 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 184    /\ wa 369   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2710
This theorem is referenced by:  r19.26-2  2840  r19.26-3  2841  ralbiim  2844  r19.27av  2845  r19.35  2857  reu8  3144  ssrab  3418  r19.28z  3760  r19.28zv  3763  r19.27z  3766  r19.27zv  3767  2ralunsn  4068  iuneq2  4175  disjxun  4278  asymref2  5203  cnvpo  5363  fncnv  5470  fnres  5515  fnopabg  5522  mpteqb  5776  eqfnfv3  5787  caoftrn  6344  abianfp  6900  iiner  7160  ixpeq2  7265  ixpin  7276  ixpfi2  7597  wemaplem2  7749  dfac5  8286  kmlem6  8312  eltsk2g  8905  intgru  8968  axgroth6  8982  fsequb  11780  rexanuz  12816  rexanre  12817  cau3lem  12825  rlimcn2  13051  o1of2  13073  o1rlimmul  13079  climbdd  13132  sqr2irr  13513  gcdcllem1  13677  pc11  13928  prmreclem2  13960  catpropd  14630  issubc3  14741  fucinv  14865  ispos2  15100  issubg3  15678  issubg4  15679  pmtrdifwrdel2  15971  iunocv  17947  tgval2  18402  1stcelcls  18906  ptclsg  19029  ptcnplem  19035  fbun  19254  txflf  19420  ucncn  19701  prdsmet  19786  metequiv  19925  metequiv2  19926  iscau4  20631  cmetcaulem  20640  evthicc2  20785  ismbfcn  20950  mbfi1flimlem  21041  rolle  21303  itgsubst  21362  plydivex  21647  ulmcaulem  21743  ulmcau  21744  ulmbdd  21747  ulmcn  21748  mumullem2  22402  2sqlem6  22592  axpasch  23009  axeuclid  23031  axcontlem2  23033  axcontlem4  23035  axcontlem7  23038  rngoueqz  23739  ocsh  24508  spanuni  24769  riesz4i  25289  leopadd  25358  leoptri  25362  leoptr  25363  disjunsn  25759  mptfnf  25799  rngsrg  26042  voliune  26498  volfiniune  26499  eulerpartlemr  26604  eulerpartlemn  26611  dfpo2  27411  poseq  27560  wfr3g  27569  wzel  27607  frr3g  27613  ovoliunnfl  28274  voliunnfl  28276  volsupnfl  28277  itg2addnc  28287  neibastop1  28421  inixp  28463  intidl  28670  mzpincl  28912  lerabdioph  28985  ltrabdioph  28988  nerabdioph  28989  dvdsrabdioph  28990  dford3lem1  29217  stoweidlem7  29645  stoweidlem54  29692  2ralbiim  29841  2reu4a  29856  ralnralall  29961  usg2wlkeq  30132  usgfiregdegfi  30371  usgreghash2spot  30505  frgrareg  30553  frgraregord013  30554  friendshipgt3  30557  ldepsnlinclem1  30753  ldepsnlinclem2  30754  pclclN  33105  tendoeq2  33988
  Copyright terms: Public domain W3C validator