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

Theorem r19.26 2989
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 457 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21ralimi 2857 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 461 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2857 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ps )
52, 4jca 532 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  -> 
( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
6 pm3.2 447 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
76ral2imi 2852 . . 3  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ( ph  /\  ps )
) )
87imp 429 . 2  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  A. x  e.  A  ( ph  /\ 
ps ) )
95, 8impbii 188 1  |-  ( A. x  e.  A  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2819
This theorem is referenced by:  r19.26-2  2990  r19.26-3  2991  ralbiim  2994  r19.27av  2995  r19.35  3008  reu8  3299  ssrab  3578  r19.28z  3920  r19.28zv  3923  r19.27z  3926  r19.27zv  3927  2ralunsn  4234  iuneq2  4342  disjxun  4445  asymref2  5382  cnvpo  5543  fncnv  5650  fnres  5695  fnopabg  5702  mpteqb  5962  eqfnfv3  5975  caoftrn  6557  iiner  7380  ixpeq2  7480  ixpin  7491  ixpfi2  7814  wemaplem2  7968  dfac5  8505  kmlem6  8531  eltsk2g  9125  intgru  9188  axgroth6  9202  fsequb  12049  rexanuz  13137  rexanre  13138  cau3lem  13146  rlimcn2  13372  o1of2  13394  o1rlimmul  13400  climbdd  13453  sqrt2irr  13839  gcdcllem1  14004  pc11  14258  prmreclem2  14290  catpropd  14961  issubc3  15072  fucinv  15196  ispos2  15431  issubg3  16014  issubg4  16015  pmtrdifwrdel2  16307  rngsrg  17024  cply1mul  18106  iunocv  18479  scmatf1  18800  cpmatsubgpmat  18988  tgval2  19224  1stcelcls  19728  ptclsg  19851  ptcnplem  19857  fbun  20076  txflf  20242  ucncn  20523  prdsmet  20608  metequiv  20747  metequiv2  20748  iscau4  21453  cmetcaulem  21462  evthicc2  21607  ismbfcn  21773  mbfi1flimlem  21864  rolle  22126  itgsubst  22185  plydivex  22427  ulmcaulem  22523  ulmcau  22524  ulmbdd  22527  ulmcn  22528  mumullem2  23182  2sqlem6  23372  axpasch  23920  axeuclid  23942  axcontlem2  23944  axcontlem4  23946  axcontlem7  23949  usg2wlkeq  24384  usgfiregdegfi  24587  usgreghash2spot  24746  frgrareg  24794  frgraregord013  24795  friendshipgt3  24798  rngoueqz  25108  ocsh  25877  spanuni  26138  riesz4i  26658  leopadd  26727  leoptri  26731  leoptr  26732  disjunsn  27126  mptfnf  27171  voliune  27841  volfiniune  27842  eulerpartlemr  27953  eulerpartlemn  27960  dfpo2  28761  poseq  28910  wfr3g  28919  wzel  28957  frr3g  28963  ovoliunnfl  29633  voliunnfl  29635  volsupnfl  29636  itg2addnc  29646  neibastop1  29780  inixp  29822  intidl  30029  mzpincl  30270  lerabdioph  30342  ltrabdioph  30345  nerabdioph  30346  dvdsrabdioph  30347  dford3lem1  30572  stoweidlem7  31307  stoweidlem54  31354  dirkercncflem3  31405  2ralbiim  31646  2reu4a  31661  ralnralall  31761  ply1mulgsumlem1  32059  ldepsnlinclem1  32187  ldepsnlinclem2  32188  pclclN  34687  tendoeq2  35570
  Copyright terms: Public domain W3C validator