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

Theorem r19.26 2984
Description: Restricted quantifier version of 19.26 1681. (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 2850 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 461 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2850 . . 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 2845 . . 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 2807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2812
This theorem is referenced by:  r19.26-2  2985  r19.26-3  2986  ralbiim  2989  r19.27v  2990  r19.35  3004  reu8  3295  ssrab  3574  r19.28z  3924  r19.28zv  3927  r19.27z  3931  r19.27zv  3932  2ralunsn  4240  iuneq2  4349  disjxun  4454  asymref2  5394  cnvpo  5551  fncnv  5658  fnres  5703  fnopabg  5710  mpteqb  5971  eqfnfv3  5984  fvn0ssdmfun  6023  caoftrn  6574  iiner  7401  ixpeq2  7502  ixpin  7513  ixpfi2  7836  wemaplem2  7990  dfac5  8526  kmlem6  8552  eltsk2g  9146  intgru  9209  axgroth6  9223  fsequb  12087  rexanuz  13189  rexanre  13190  cau3lem  13198  rlimcn2  13424  o1of2  13446  o1rlimmul  13452  climbdd  13505  sqrt2irr  13993  gcdcllem1  14160  pc11  14414  prmreclem2  14446  catpropd  15124  issubc3  15264  fucinv  15388  ispos2  15703  issubg3  16345  issubg4  16346  pmtrdifwrdel2  16637  ringsrg  17363  cply1mul  18461  iunocv  18838  scmatf1  19159  cpmatsubgpmat  19347  tgval2  19583  1stcelcls  20087  ptclsg  20241  ptcnplem  20247  fbun  20466  txflf  20632  ucncn  20913  prdsmet  20998  metequiv  21137  metequiv2  21138  iscau4  21843  cmetcaulem  21852  evthicc2  21997  ismbfcn  22163  mbfi1flimlem  22254  rolle  22516  itgsubst  22575  plydivex  22818  ulmcaulem  22914  ulmcau  22915  ulmbdd  22918  ulmcn  22919  mumullem2  23579  2sqlem6  23769  axpasch  24370  axeuclid  24392  axcontlem2  24394  axcontlem4  24396  axcontlem7  24399  usg2wlkeq  24834  usgfiregdegfi  25037  usgreghash2spot  25195  frgrareg  25243  frgraregord013  25244  friendshipgt3  25247  rngoueqz  25558  ocsh  26327  spanuni  26588  riesz4i  27108  leopadd  27177  leoptri  27181  leoptr  27182  disjunsn  27590  mptfnf  27642  voliune  28362  volfiniune  28363  eulerpartlemr  28488  eulerpartlemn  28495  dfpo2  29359  poseq  29507  wfr3g  29516  wzel  29554  frr3g  29560  ovoliunnfl  30218  voliunnfl  30220  volsupnfl  30221  itg2addnc  30231  neibastop1  30339  inixp  30381  intidl  30588  mzpincl  30828  lerabdioph  30900  ltrabdioph  30903  nerabdioph  30904  dvdsrabdioph  30905  dford3lem1  31130  stoweidlem7  31950  stoweidlem54  31997  dirkercncflem3  32048  2ralbiim  32340  2reu4a  32355  ralnralall  32516  ply1mulgsumlem1  33088  ldepsnlinclem1  33208  ldepsnlinclem2  33209  pclclN  35716  tendoeq2  36601
  Copyright terms: Public domain W3C validator