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

Theorem r19.26 2688
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 443 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21ralimi 2631 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 447 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2631 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ps )
52, 4jca 518 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  -> 
( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
6 pm3.2 434 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
76ral2imi 2632 . . 3  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ( ph  /\  ps )
) )
87imp 418 . 2  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  A. x  e.  A  ( ph  /\ 
ps ) )
95, 8impbii 180 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 176    /\ wa 358   A.wral 2556
This theorem is referenced by:  r19.26-2  2689  r19.26-3  2690  ralbiim  2693  r19.27av  2694  r19.35  2700  reu8  2974  ssrab  3264  r19.28z  3559  r19.28zv  3562  r19.27z  3565  r19.27zv  3566  2ralunsn  3832  iuneq2  3937  disjxun  4037  asymref2  5076  cnvpo  5229  fncnv  5330  fnres  5376  fnopabg  5383  mpteqb  5630  eqfnfv3  5640  caoftrn  6128  abianfp  6487  iiner  6747  ixpeq2  6846  ixpin  6857  ixpfi2  7170  wemaplem2  7278  dfac5  7771  kmlem6  7797  eltsk2g  8389  intgru  8452  axgroth6  8466  fsequb  11053  rexanuz  11845  rexanre  11846  cau3lem  11854  rlimcn2  12080  o1of2  12102  o1rlimmul  12108  sqr2irr  12543  gcdcllem1  12706  pc11  12948  prmreclem2  12980  catpropd  13628  issubc3  13739  fucinv  13863  ispos2  14098  issubg3  14653  issubg4  14654  iunocv  16597  tgval2  16710  1stcelcls  17203  ptclsg  17325  ptcnplem  17331  fbun  17551  txflf  17717  prdsmet  17950  metequiv  18071  metequiv2  18072  iscau4  18721  cmetcaulem  18730  evthicc2  18836  ismbfcn  19002  mbfi1flimlem  19093  rolle  19353  itgsubst  19412  plydivex  19693  ulmcaulem  19787  ulmcau  19788  ulmbdd  19791  ulmcn  19792  mumullem2  20434  2sqlem6  20624  rngoueqz  21113  ocsh  21878  spanuni  22139  riesz4i  22659  leopadd  22728  leoptri  22732  leoptr  22733  mptfnf  23241  dfpo2  24183  poseq  24324  wfr3g  24326  frr3g  24351  axpasch  24641  axeuclid  24663  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  ovoliunnfl  25001  itg2addnc  25005  r19.26-2a  25037  domintrefb  25166  celsor  25214  domintrefc  25228  svli2  25587  inttop2  25618  qusp  25645  tartarmap  25991  neibastop1  26411  inixp  26502  intidl  26757  mzpincl  26915  lerabdioph  26989  ltrabdioph  26992  nerabdioph  26993  dvdsrabdioph  26994  dford3lem1  27222  stoweidlem7  27859  stoweidlem54  27906  stoweidlem59  27911  2ralbiim  28055  2reu4a  28070  pclclN  30702  tendoeq2  31585
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2561
  Copyright terms: Public domain W3C validator