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

Theorem r19.26 2675
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 2618 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 447 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2618 . . 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 2619 . . 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 2543
This theorem is referenced by:  r19.26-2  2676  r19.26-3  2677  ralbiim  2680  r19.27av  2681  r19.35  2687  reu8  2961  ssrab  3251  r19.28z  3546  r19.28zv  3549  r19.27z  3552  r19.27zv  3553  2ralunsn  3816  iuneq2  3921  disjxun  4021  asymref2  5060  cnvpo  5213  fncnv  5314  fnres  5360  fnopabg  5367  mpteqb  5614  eqfnfv3  5624  caoftrn  6112  abianfp  6471  iiner  6731  ixpeq2  6830  ixpin  6841  ixpfi2  7154  wemaplem2  7262  dfac5  7755  kmlem6  7781  eltsk2g  8373  intgru  8436  axgroth6  8450  fsequb  11037  rexanuz  11829  rexanre  11830  cau3lem  11838  rlimcn2  12064  o1of2  12086  o1rlimmul  12092  sqr2irr  12527  gcdcllem1  12690  pc11  12932  prmreclem2  12964  catpropd  13612  issubc3  13723  fucinv  13847  ispos2  14082  issubg3  14637  issubg4  14638  iunocv  16581  tgval2  16694  1stcelcls  17187  ptclsg  17309  ptcnplem  17315  fbun  17535  txflf  17701  prdsmet  17934  metequiv  18055  metequiv2  18056  iscau4  18705  cmetcaulem  18714  evthicc2  18820  ismbfcn  18986  mbfi1flimlem  19077  rolle  19337  itgsubst  19396  plydivex  19677  ulmcaulem  19771  ulmcau  19772  ulmbdd  19775  ulmcn  19776  mumullem2  20418  2sqlem6  20608  rngoueqz  21097  ocsh  21862  spanuni  22123  riesz4i  22643  leopadd  22712  leoptri  22716  leoptr  22717  mptfnf  23226  dfpo2  24112  poseq  24253  wfr3g  24255  frr3g  24280  axpasch  24569  axeuclid  24591  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  r19.26-2a  24934  domintrefb  25063  celsor  25111  domintrefc  25125  svli2  25484  inttop2  25515  qusp  25542  tartarmap  25888  neibastop1  26308  inixp  26399  intidl  26654  mzpincl  26812  lerabdioph  26886  ltrabdioph  26889  nerabdioph  26890  dvdsrabdioph  26891  dford3lem1  27119  stoweidlem7  27756  stoweidlem54  27803  stoweidlem59  27808  2ralbiim  27952  2reu4a  27967  pclclN  30080  tendoeq2  30963
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ral 2548
  Copyright terms: Public domain W3C validator