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

Theorem r19.26 2953
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 2818 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 461 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2818 . . 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 2813 . . 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 2798
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2803
This theorem is referenced by:  r19.26-2  2954  r19.26-3  2955  ralbiim  2958  r19.27av  2959  r19.35  2971  reu8  3260  ssrab  3537  r19.28z  3879  r19.28zv  3882  r19.27z  3885  r19.27zv  3886  2ralunsn  4187  iuneq2  4294  disjxun  4397  asymref2  5322  cnvpo  5482  fncnv  5589  fnres  5634  fnopabg  5641  mpteqb  5896  eqfnfv3  5907  caoftrn  6464  iiner  7281  ixpeq2  7386  ixpin  7397  ixpfi2  7719  wemaplem2  7871  dfac5  8408  kmlem6  8434  eltsk2g  9028  intgru  9091  axgroth6  9105  fsequb  11913  rexanuz  12950  rexanre  12951  cau3lem  12959  rlimcn2  13185  o1of2  13207  o1rlimmul  13213  climbdd  13266  sqr2irr  13648  gcdcllem1  13812  pc11  14063  prmreclem2  14095  catpropd  14766  issubc3  14877  fucinv  15001  ispos2  15236  issubg3  15817  issubg4  15818  pmtrdifwrdel2  16110  rngsrg  16805  iunocv  18230  tgval2  18692  1stcelcls  19196  ptclsg  19319  ptcnplem  19325  fbun  19544  txflf  19710  ucncn  19991  prdsmet  20076  metequiv  20215  metequiv2  20216  iscau4  20921  cmetcaulem  20930  evthicc2  21075  ismbfcn  21241  mbfi1flimlem  21332  rolle  21594  itgsubst  21653  plydivex  21895  ulmcaulem  21991  ulmcau  21992  ulmbdd  21995  ulmcn  21996  mumullem2  22650  2sqlem6  22840  axpasch  23338  axeuclid  23360  axcontlem2  23362  axcontlem4  23364  axcontlem7  23367  rngoueqz  24068  ocsh  24837  spanuni  25098  riesz4i  25618  leopadd  25687  leoptri  25691  leoptr  25692  disjunsn  26086  mptfnf  26126  voliune  26788  volfiniune  26789  eulerpartlemr  26900  eulerpartlemn  26907  dfpo2  27708  poseq  27857  wfr3g  27866  wzel  27904  frr3g  27910  ovoliunnfl  28580  voliunnfl  28582  volsupnfl  28583  itg2addnc  28593  neibastop1  28727  inixp  28769  intidl  28976  mzpincl  29217  lerabdioph  29290  ltrabdioph  29293  nerabdioph  29294  dvdsrabdioph  29295  dford3lem1  29522  stoweidlem7  29949  stoweidlem54  29996  2ralbiim  30145  2reu4a  30160  ralnralall  30265  usg2wlkeq  30436  usgfiregdegfi  30675  usgreghash2spot  30809  frgrareg  30857  frgraregord013  30858  friendshipgt3  30861  ply1mulgsumlem1  30997  cply1mul  31004  ldepsnlinclem1  31165  ldepsnlinclem2  31166  cpmatsubgpmat  31195  pclclN  33858  tendoeq2  34741
  Copyright terms: Public domain W3C validator