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

Theorem r19.26 2637
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 2580 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 449 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2580 . . 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 2581 . . 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 2509
This theorem is referenced by:  r19.26-2  2638  r19.26-3  2639  ralbiim  2642  r19.27av  2643  r19.35  2649  reu8  2900  ssrab  3172  r19.28z  3452  r19.28zv  3455  r19.27z  3458  r19.27zv  3459  2ralunsn  3716  iuneq2  3819  disjxun  3918  asymref2  4967  cnvpo  5119  fncnv  5171  fnres  5217  fnopabg  5224  mpteqb  5466  eqfnfv3  5476  caoftrn  5964  abianfp  6357  iiner  6617  ixpeq2  6716  ixpin  6727  ixpfi2  7038  wemaplem2  7146  dfac5  7639  kmlem6  7665  eltsk2g  8253  intgru  8316  axgroth6  8330  fsequb  10915  rexanuz  11706  rexanre  11707  cau3lem  11715  rlimcn2  11941  o1of2  11963  o1rlimmul  11969  sqr2irr  12401  gcdcllem1  12564  pc11  12806  prmreclem2  12838  catpropd  13456  issubc3  13567  fucinv  13691  ispos2  13926  issubg3  14472  issubg4  14473  iunocv  16413  tgval2  16526  1stcelcls  17019  ptclsg  17141  ptcnplem  17147  fbun  17367  txflf  17533  prdsmet  17766  metequiv  17887  metequiv2  17888  iscau4  18537  cmetcaulem  18546  evthicc2  18652  ismbfcn  18818  mbfi1flimlem  18909  rolle  19169  itgsubst  19228  plydivex  19509  ulmcaulem  19603  ulmcau  19604  ulmbdd  19607  ulmcn  19608  mumullem2  20250  2sqlem6  20440  rngoueqz  20927  ocsh  21692  spanuni  21953  riesz4i  22473  leopadd  22542  leoptri  22546  leoptr  22547  dfpo2  23282  poseq  23421  wfr3g  23423  frr3g  23448  axpasch  23743  axeuclid  23765  axcontlem2  23767  axcontlem4  23769  axcontlem7  23772  r19.26-2a  24099  domintrefb  24228  celsor  24276  domintrefc  24291  svli2  24650  inttop2  24681  qusp  24708  tartarmap  25054  neibastop1  25474  inixp  25565  intidl  25820  mzpincl  25978  lerabdioph  26052  ltrabdioph  26055  nerabdioph  26056  dvdsrabdioph  26057  dford3lem1  26285  pclclN  28769  tendoeq2  29652
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 2513
  Copyright terms: Public domain W3C validator