Theorem raleq 3115

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

Assertion

Ref	Expression
raleq	⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleq

Step	Hyp	Ref	Expression
1		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	raleqf 3111	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901

This theorem is referenced by:  raleqi  3119  raleqdv  3121  raleqbi1dv  3123  sbralie  3160  r19.2zb  4013  inteq  4413  iineq1  4471  fri  5000  frsn  5112  fncnv  5876  isoeq4  6470  onminex  6899  tfinds  6951  f1oweALT  7043  frxp  7174  wfrlem1  7301  wfrlem15  7316  tfrlem1  7359  tfrlem12  7372  omeulem1  7549  ixpeq1  7805  undifixp  7830  ac6sfi  8089  frfi  8090  iunfi  8137  indexfi  8157  supeq1  8234  supeq2  8237  bnd2  8639  acneq  8749  aceq3lem  8826  dfac5lem4  8832  dfac8  8840  dfac9  8841  kmlem1  8855  kmlem10  8864  kmlem13  8867  cfval  8952  axcc2lem  9141  axcc4dom  9146  axdc3lem3  9157  axdc3lem4  9158  ac4c  9181  ac5  9182  ac6sg  9193  zorn2lem7  9207  xrsupsslem  12009  xrinfmsslem  12010  xrsupss  12011  xrinfmss  12012  fsuppmapnn0fiubex  12654  rexanuz  13933  rexfiuz  13935  modfsummod  14367  gcdcllem3  15061  lcmfval  15172  lcmf0val  15173  lcmfunsnlem  15192  coprmprod  15213  coprmproddvds  15215  isprs  16753  drsdirfi  16761  isdrs2  16762  ispos  16770  lubeldm  16804  lubval  16807  glbeldm  16817  glbval  16820  istos  16858  pospropd  16957  isdlat  17016  mgm0  17078  sgrp0  17114  mhmpropd  17164  isghm  17483  cntzval  17577  efgval  17953  iscmn  18023  dfrhm2  18540  lidldvgen  19076  coe1fzgsumd  19493  evl1gsumd  19542  ocvval  19830  isobs  19883  mat0dimcrng  20095  mdetunilem9  20245  ist0  20934  cmpcovf  21004  is1stc  21054  2ndc1stc  21064  isref  21122  txflf  21620  ustuqtop4  21858  iscfilu  21902  ispsmet  21919  ismet  21938  isxmet  21939  cncfval  22499  lebnumlem3  22570  fmcfil  22878  iscfil3  22879  caucfil  22889  iscmet3  22899  cfilres  22902  minveclem3  23008  ovolfiniun  23076  finiunmbl  23119  volfiniun  23122  dvcn  23490  ulmval  23938  axtgcont1  25167  tgcgr4  25226  nb3grapr  25982  rusgrasn  26472  isplig  26720  isgrpo  26735  isablo  26784  ocval  27523  acunirnmpt  28841  isomnd  29032  isorng  29130  ismbfm  29641  isanmbfm  29645  bnj865  30247  bnj1154  30321  bnj1296  30343  bnj1463  30377  derangval  30403  setinds  30927  dfon2lem3  30934  dfon2lem7  30938  tfisg  30960  poseq  30994  frrlem1  31024  sltval2  31053  sltres  31061  nodense  31088  nobndup  31099  nobnddown  31100  nofulllem1  31101  dfrecs2  31227  dfrdg4  31228  isfne  31504  finixpnum  32564  mblfinlem1  32616  mbfresfi  32626  indexdom  32699  heibor1lem  32778  isexid2  32824  ismndo2  32843  rngomndo  32904  pridl  33006  smprngopr  33021  ispridlc  33039  setindtrs  36610  dford3lem2  36612  dfac11  36650  fnchoice  38211  axccdom  38411  axccd  38424  stoweidlem31  38924  stoweidlem57  38950  fourierdlem80  39079  fourierdlem103  39102  fourierdlem104  39103  issal  39210  isvonmbl  39528  nb3grpr  40610  cplgr0v  40649  dfconngr1  41355  isconngr  41356  0vconngr  41360  1conngr  41361  frgr0v  41433  mgmhmpropd  41575  rnghmval  41681  zrrnghm  41707  bnd2d  42226