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

Theorem r19.26 2648
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 2591 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 449 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2591 . . 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 2592 . . 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 2516
This theorem is referenced by:  r19.26-2  2649  r19.26-3  2650  ralbiim  2653  r19.27av  2654  r19.35  2660  reu8  2929  ssrab  3212  r19.28z  3507  r19.28zv  3510  r19.27z  3513  r19.27zv  3514  2ralunsn  3776  iuneq2  3881  disjxun  3981  asymref2  5034  cnvpo  5186  fncnv  5238  fnres  5284  fnopabg  5291  mpteqb  5534  eqfnfv3  5544  caoftrn  6032  abianfp  6425  iiner  6685  ixpeq2  6784  ixpin  6795  ixpfi2  7108  wemaplem2  7216  dfac5  7709  kmlem6  7735  eltsk2g  8327  intgru  8390  axgroth6  8404  fsequb  10989  rexanuz  11780  rexanre  11781  cau3lem  11789  rlimcn2  12015  o1of2  12037  o1rlimmul  12043  sqr2irr  12475  gcdcllem1  12638  pc11  12880  prmreclem2  12912  catpropd  13560  issubc3  13671  fucinv  13795  ispos2  14030  issubg3  14585  issubg4  14586  iunocv  16529  tgval2  16642  1stcelcls  17135  ptclsg  17257  ptcnplem  17263  fbun  17483  txflf  17649  prdsmet  17882  metequiv  18003  metequiv2  18004  iscau4  18653  cmetcaulem  18662  evthicc2  18768  ismbfcn  18934  mbfi1flimlem  19025  rolle  19285  itgsubst  19344  plydivex  19625  ulmcaulem  19719  ulmcau  19720  ulmbdd  19723  ulmcn  19724  mumullem2  20366  2sqlem6  20556  rngoueqz  21043  ocsh  21808  spanuni  22069  riesz4i  22589  leopadd  22658  leoptri  22662  leoptr  22663  dfpo2  23469  poseq  23608  wfr3g  23610  frr3g  23635  axpasch  23930  axeuclid  23952  axcontlem2  23954  axcontlem4  23956  axcontlem7  23959  r19.26-2a  24286  domintrefb  24415  celsor  24463  domintrefc  24478  svli2  24837  inttop2  24868  qusp  24895  tartarmap  25241  neibastop1  25661  inixp  25752  intidl  26007  mzpincl  26165  lerabdioph  26239  ltrabdioph  26242  nerabdioph  26243  dvdsrabdioph  26244  dford3lem1  26472  stoweidlem7  27077  stoweidlem54  27124  stoweidlem59  27129  pclclN  29231  tendoeq2  30114
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536
This theorem depends on definitions:  df-bi 179  df-an 362  df-ral 2521
  Copyright terms: Public domain W3C validator