Theorem r19.26 3064

Description: Restricted quantifier version of 19.26 1798. (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

Step	Hyp	Ref	Expression
1		simpl 473	. . . 4 |- ( ( ph /\ ps ) -> ph )
2	1	ralimi 2952	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ph )
3		simpr 477	. . . 4 |- ( ( ph /\ ps ) -> ps )
4	3	ralimi 2952	. . 3 |- ( A. x e. A ( ph /\ ps ) -> A. x e. A ps )
5	2, 4	jca 554	. 2 |- ( A. x e. A ( ph /\ ps ) -> ( A. x e. A ph /\ A. x e. A ps ) )
6		pm3.2 463	. . . 4 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
7	6	ral2imi 2947	. . 3 |- ( A. x e. A ph -> ( A. x e. A ps -> A. x e. A ( ph /\ ps ) ) )
8	7	imp 445	. 2 |- ( ( A. x e. A ph /\ A. x e. A ps ) -> A. x e. A ( ph /\ ps ) )
9	5, 8	impbii 199	1 |- ( A. x e. A ( ph /\ ps ) <-> ( A. x e. A ph /\ A. x e. A ps ) )

Syntax hints:   <-> wb 196   /\ wa 384   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ral 2917

This theorem is referenced by:  r19.26-2  3065  r19.26-3  3066  ralbiim  3069  r19.27v  3070  r19.35  3084  reu8  3402  ssrab  3680  r19.28z  4063  r19.27z  4070  ralnralall  4080  ssdifsn  4318  2ralunsn  4423  iuneq2  4537  disjxun  4651  asymref2  5513  cnvpo  5673  fncnv  5962  fnres  6007  mptfnf  6015  fnopabg  6017  mpteqb  6299  eqfnfv3  6313  fvn0ssdmfun  6350  caoftrn  6932  wfr3g  7413  iiner  7819  ixpeq2  7922  ixpin  7933  ixpfi2  8264  wemaplem2  8452  dfac5  8951  kmlem6  8977  eltsk2g  9573  intgru  9636  axgroth6  9650  fsequb  12774  rexanuz  14085  rexanre  14086  cau3lem  14094  rlimcn2  14321  o1of2  14343  o1rlimmul  14349  climbdd  14402  sqrt2irr  14979  gcdcllem1  15221  pc11  15584  prmreclem2  15621  catpropd  16369  issubc3  16509  fucinv  16633  ispos2  16948  issubg3  17612  issubg4  17613  pmtrdifwrdel2  17906  ringsrg  18589  cply1mul  19664  iunocv  20025  scmatf1  20337  cpmatsubgpmat  20525  tgval2  20760  1stcelcls  21264  ptclsg  21418  ptcnplem  21424  fbun  21644  txflf  21810  ucncn  22089  prdsmet  22175  metequiv  22314  metequiv2  22315  ncvsi  22951  iscau4  23077  cmetcaulem  23086  evthicc2  23229  ismbfcn  23398  mbfi1flimlem  23489  rolle  23753  itgsubst  23812  plydivex  24052  ulmcaulem  24148  ulmcau  24149  ulmbdd  24152  ulmcn  24153  mumullem2  24906  2sqlem6  25148  tgcgr4  25426  axpasch  25821  axeuclid  25843  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  vtxd0nedgb  26384  fusgrregdegfi  26465  rusgr1vtxlem  26483  uspgr2wlkeq  26542  wlkdlem4  26582  lfgriswlk  26585  frgrreg  27252  frgrregord013  27253  friendshipgt3  27256  ocsh  28142  spanuni  28403  riesz4i  28922  leopadd  28991  leoptri  28995  leoptr  28996  disjunsn  29407  voliune  30292  volfiniune  30293  eulerpartlemr  30436  eulerpartlemn  30443  dfpo2  31645  poseq  31750  wzel  31771  wzelOLD  31772  frr3g  31779  ssltun2  31916  neibastop1  32354  phpreu  33393  ptrecube  33409  poimirlem23  33432  poimirlem27  33436  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  itg2addnc  33464  inixp  33523  rngoueqz  33739  intidl  33828  pclclN  35177  tendoeq2  36062  mzpincl  37297  lerabdioph  37369  ltrabdioph  37372  nerabdioph  37373  dvdsrabdioph  37374  dford3lem1  37593  gneispace  38432  ssrabf  39298  climxrre  39982  stoweidlem7  40224  stoweidlem54  40271  dirkercncflem3  40322  2ralbiim  41174  2reu4a  41189  ply1mulgsumlem1  42174  ldepsnlinclem1  42294  ldepsnlinclem2  42295