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

Theorem r19.26 2844
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 2786 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 461 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2786 . . 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 2787 . . 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 2710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2715
This theorem is referenced by:  r19.26-2  2845  r19.26-3  2846  ralbiim  2849  r19.27av  2850  r19.35  2862  reu8  3150  ssrab  3425  r19.28z  3767  r19.28zv  3770  r19.27z  3773  r19.27zv  3774  2ralunsn  4075  iuneq2  4182  disjxun  4285  asymref2  5210  cnvpo  5370  fncnv  5477  fnres  5522  fnopabg  5529  mpteqb  5783  eqfnfv3  5794  caoftrn  6350  iiner  7164  ixpeq2  7269  ixpin  7280  ixpfi2  7601  wemaplem2  7753  dfac5  8290  kmlem6  8316  eltsk2g  8910  intgru  8973  axgroth6  8987  fsequb  11789  rexanuz  12825  rexanre  12826  cau3lem  12834  rlimcn2  13060  o1of2  13082  o1rlimmul  13088  climbdd  13141  sqr2irr  13523  gcdcllem1  13687  pc11  13938  prmreclem2  13970  catpropd  14640  issubc3  14751  fucinv  14875  ispos2  15110  issubg3  15690  issubg4  15691  pmtrdifwrdel2  15983  rngsrg  16673  iunocv  18086  tgval2  18541  1stcelcls  19045  ptclsg  19168  ptcnplem  19174  fbun  19393  txflf  19559  ucncn  19840  prdsmet  19925  metequiv  20064  metequiv2  20065  iscau4  20770  cmetcaulem  20779  evthicc2  20924  ismbfcn  21089  mbfi1flimlem  21180  rolle  21442  itgsubst  21501  plydivex  21743  ulmcaulem  21839  ulmcau  21840  ulmbdd  21843  ulmcn  21844  mumullem2  22498  2sqlem6  22688  axpasch  23155  axeuclid  23177  axcontlem2  23179  axcontlem4  23181  axcontlem7  23184  rngoueqz  23885  ocsh  24654  spanuni  24915  riesz4i  25435  leopadd  25504  leoptri  25508  leoptr  25509  disjunsn  25904  mptfnf  25944  voliune  26614  volfiniune  26615  eulerpartlemr  26726  eulerpartlemn  26733  dfpo2  27534  poseq  27683  wfr3g  27692  wzel  27730  frr3g  27736  ovoliunnfl  28404  voliunnfl  28406  volsupnfl  28407  itg2addnc  28417  neibastop1  28551  inixp  28593  intidl  28800  mzpincl  29041  lerabdioph  29114  ltrabdioph  29117  nerabdioph  29118  dvdsrabdioph  29119  dford3lem1  29346  stoweidlem7  29773  stoweidlem54  29820  2ralbiim  29969  2reu4a  29984  ralnralall  30089  usg2wlkeq  30260  usgfiregdegfi  30499  usgreghash2spot  30633  frgrareg  30681  frgraregord013  30682  friendshipgt3  30685  ldepsnlinclem1  30978  ldepsnlinclem2  30979  pclclN  33428  tendoeq2  34311
  Copyright terms: Public domain W3C validator