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

Theorem r19.26 2838
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 2781 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 448 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2781 . . 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 2782 . . 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 2705
This theorem is referenced by:  r19.26-2  2839  r19.26-3  2840  ralbiim  2843  r19.27av  2844  r19.35  2855  reu8  3130  ssrab  3421  r19.28z  3720  r19.28zv  3723  r19.27z  3726  r19.27zv  3727  2ralunsn  4004  iuneq2  4109  disjxun  4210  asymref2  5251  cnvpo  5410  fncnv  5515  fnres  5561  fnopabg  5568  mpteqb  5819  eqfnfv3  5829  caoftrn  6339  abianfp  6716  iiner  6976  ixpeq2  7076  ixpin  7087  ixpfi2  7405  wemaplem2  7516  dfac5  8009  kmlem6  8035  eltsk2g  8626  intgru  8689  axgroth6  8703  fsequb  11314  rexanuz  12149  rexanre  12150  cau3lem  12158  rlimcn2  12384  o1of2  12406  o1rlimmul  12412  climbdd  12465  sqr2irr  12848  gcdcllem1  13011  pc11  13253  prmreclem2  13285  catpropd  13935  issubc3  14046  fucinv  14170  ispos2  14405  issubg3  14960  issubg4  14961  iunocv  16908  tgval2  17021  1stcelcls  17524  ptclsg  17647  ptcnplem  17653  fbun  17872  txflf  18038  ucncn  18315  prdsmet  18400  metequiv  18539  metequiv2  18540  iscau4  19232  cmetcaulem  19241  evthicc2  19357  ismbfcn  19523  mbfi1flimlem  19614  rolle  19874  itgsubst  19933  plydivex  20214  ulmcaulem  20310  ulmcau  20311  ulmbdd  20314  ulmcn  20315  mumullem2  20963  2sqlem6  21153  rngoueqz  22018  ocsh  22785  spanuni  23046  riesz4i  23566  leopadd  23635  leoptri  23639  leoptr  23640  mptfnf  24073  voliune  24585  volfiniune  24586  dfpo2  25378  poseq  25528  wfr3g  25537  wzel  25575  frr3g  25581  axpasch  25880  axeuclid  25902  axcontlem2  25904  axcontlem4  25906  axcontlem7  25909  ovoliunnfl  26248  voliunnfl  26250  volsupnfl  26251  itg2addnc  26259  neibastop1  26388  inixp  26430  intidl  26639  mzpincl  26791  lerabdioph  26865  ltrabdioph  26868  nerabdioph  26869  dvdsrabdioph  26870  dford3lem1  27097  stoweidlem7  27732  stoweidlem54  27779  2ralbiim  27928  2reu4a  27943  usg2wlkeq  28304  usgfiregdegfi  28361  usgreghash2spot  28458  pclclN  30688  tendoeq2  31571
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 2710
  Copyright terms: Public domain W3C validator