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

Theorem r19.26 2646
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 2589 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 449 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2589 . . 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 2590 . . 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  2647  r19.26-3  2648  ralbiim  2651  r19.27av  2652  r19.35  2658  reu8  2914  ssrab  3193  r19.28z  3488  r19.28zv  3491  r19.27z  3494  r19.27zv  3495  2ralunsn  3757  iuneq2  3862  disjxun  3961  asymref2  5013  cnvpo  5165  fncnv  5217  fnres  5263  fnopabg  5270  mpteqb  5513  eqfnfv3  5523  caoftrn  6011  abianfp  6404  iiner  6664  ixpeq2  6763  ixpin  6774  ixpfi2  7087  wemaplem2  7195  dfac5  7688  kmlem6  7714  eltsk2g  8306  intgru  8369  axgroth6  8383  fsequb  10968  rexanuz  11759  rexanre  11760  cau3lem  11768  rlimcn2  11994  o1of2  12016  o1rlimmul  12022  sqr2irr  12454  gcdcllem1  12617  pc11  12859  prmreclem2  12891  catpropd  13539  issubc3  13650  fucinv  13774  ispos2  14009  issubg3  14564  issubg4  14565  iunocv  16508  tgval2  16621  1stcelcls  17114  ptclsg  17236  ptcnplem  17242  fbun  17462  txflf  17628  prdsmet  17861  metequiv  17982  metequiv2  17983  iscau4  18632  cmetcaulem  18641  evthicc2  18747  ismbfcn  18913  mbfi1flimlem  19004  rolle  19264  itgsubst  19323  plydivex  19604  ulmcaulem  19698  ulmcau  19699  ulmbdd  19702  ulmcn  19703  mumullem2  20345  2sqlem6  20535  rngoueqz  21022  ocsh  21787  spanuni  22048  riesz4i  22568  leopadd  22637  leoptri  22641  leoptr  22642  dfpo2  23448  poseq  23587  wfr3g  23589  frr3g  23614  axpasch  23909  axeuclid  23931  axcontlem2  23933  axcontlem4  23935  axcontlem7  23938  r19.26-2a  24265  domintrefb  24394  celsor  24442  domintrefc  24457  svli2  24816  inttop2  24847  qusp  24874  tartarmap  25220  neibastop1  25640  inixp  25731  intidl  25986  mzpincl  26144  lerabdioph  26218  ltrabdioph  26221  nerabdioph  26222  dvdsrabdioph  26223  dford3lem1  26451  stoweidlem7  27056  stoweidlem54  27103  stoweidlem59  27108  pclclN  29210  tendoeq2  30093
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 2520
  Copyright terms: Public domain W3C validator