Theorem raleq 3138

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)

Assertion

Ref	Expression
raleq	|- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) )

Distinct variable groups:   x, A   x, B

Allowed substitution hint:   ph( x)

Proof of Theorem raleq

Step	Hyp	Ref	Expression
1		nfcv 2764	. 2 |- F/_ x A
2		nfcv 2764	. 2 |- F/_ x B
3	1, 2	raleqf 3134	1 |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   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  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917

This theorem is referenced by:  raleqi  3142  raleqdv  3144  raleqbi1dv  3146  sbralie  3184  r19.2zb  4061  inteq  4478  iineq1  4535  fri  5076  frsn  5189  fncnv  5962  isoeq4  6570  onminex  7007  tfinds  7059  f1oweALT  7152  frxp  7287  wfrlem1  7414  wfrlem15  7429  tfrlem1  7472  tfrlem12  7485  omeulem1  7662  ixpeq1  7919  undifixp  7944  ac6sfi  8204  frfi  8205  iunfi  8254  indexfi  8274  supeq1  8351  supeq2  8354  bnd2  8756  acneq  8866  aceq3lem  8943  dfac5lem4  8949  dfac8  8957  dfac9  8958  kmlem1  8972  kmlem10  8981  kmlem13  8984  cfval  9069  axcc2lem  9258  axcc4dom  9263  axdc3lem3  9274  axdc3lem4  9275  ac4c  9298  ac5  9299  ac6sg  9310  zorn2lem7  9324  xrsupsslem  12137  xrinfmsslem  12138  xrsupss  12139  xrinfmss  12140  fsuppmapnn0fiubex  12792  rexanuz  14085  rexfiuz  14087  modfsummod  14526  gcdcllem3  15223  lcmfval  15334  lcmf0val  15335  lcmfunsnlem  15354  coprmprod  15375  coprmproddvds  15377  isprs  16930  drsdirfi  16938  isdrs2  16939  ispos  16947  lubeldm  16981  lubval  16984  glbeldm  16994  glbval  16997  istos  17035  pospropd  17134  isdlat  17193  mhmpropd  17341  isghm  17660  cntzval  17754  efgval  18130  iscmn  18200  dfrhm2  18717  lidldvgen  19255  coe1fzgsumd  19672  evl1gsumd  19721  ocvval  20011  isobs  20064  mat0dimcrng  20276  mdetunilem9  20426  ist0  21124  cmpcovf  21194  is1stc  21244  2ndc1stc  21254  isref  21312  txflf  21810  ustuqtop4  22048  iscfilu  22092  ispsmet  22109  ismet  22128  isxmet  22129  cncfval  22691  lebnumlem3  22762  fmcfil  23070  iscfil3  23071  caucfil  23081  iscmet3  23091  cfilres  23094  minveclem3  23200  ovolfiniun  23269  finiunmbl  23312  volfiniun  23315  dvcn  23684  ulmval  24134  axtgcont1  25367  tgcgr4  25426  nb3grpr  26284  dfconngr1  27048  isconngr  27049  1conngr  27054  frgr0v  27125  isplig  27328  isgrpo  27351  isablo  27400  ocval  28139  acunirnmpt  29459  isomnd  29701  isorng  29799  ismbfm  30314  isanmbfm  30318  bnj865  30993  bnj1154  31067  bnj1296  31089  bnj1463  31123  derangval  31149  setinds  31683  dfon2lem3  31690  dfon2lem7  31694  tfisg  31716  poseq  31750  frrlem1  31780  sltval2  31809  sltres  31815  nolesgn2o  31824  nodense  31842  nosupbnd2lem1  31861  brsslt  31900  dfrecs2  32057  dfrdg4  32058  isfne  32334  finixpnum  33394  mblfinlem1  33446  mbfresfi  33456  indexdom  33529  heibor1lem  33608  isexid2  33654  ismndo2  33673  rngomndo  33734  pridl  33836  smprngopr  33851  ispridlc  33869  setindtrs  37592  dford3lem2  37594  dfac11  37632  fnchoice  39188  axccdom  39416  axccd  39429  stoweidlem31  40248  stoweidlem57  40274  fourierdlem80  40403  fourierdlem103  40426  fourierdlem104  40427  isvonmbl  40852  mgmhmpropd  41785  rnghmval  41891  zrrnghm  41917  bnd2d  42428