Theorem raleq 3168

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 2793	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2793	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	raleqf 3164	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523  ∀wral 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946

This theorem is referenced by:  raleqi  3172  raleqdv  3174  raleqbi1dv  3176  sbralie  3214  r19.2zb  4094  inteq  4510  iineq1  4567  fri  5105  frsn  5223  fncnv  6000  isoeq4  6610  onminex  7049  tfinds  7101  f1oweALT  7194  frxp  7332  wfrlem1  7459  wfrlem15  7474  tfrlem1  7517  tfrlem12  7530  omeulem1  7707  ixpeq1  7961  undifixp  7986  ac6sfi  8245  frfi  8246  iunfi  8295  indexfi  8315  supeq1  8392  supeq2  8395  bnd2  8794  acneq  8904  aceq3lem  8981  dfac5lem4  8987  dfac8  8995  dfac9  8996  kmlem1  9010  kmlem10  9019  kmlem13  9022  cfval  9107  axcc2lem  9296  axcc4dom  9301  axdc3lem3  9312  axdc3lem4  9313  ac4c  9336  ac5  9337  ac6sg  9348  zorn2lem7  9362  xrsupsslem  12175  xrinfmsslem  12176  xrsupss  12177  xrinfmss  12178  fsuppmapnn0fiubex  12832  rexanuz  14129  rexfiuz  14131  modfsummod  14570  gcdcllem3  15270  lcmfval  15381  lcmf0val  15382  lcmfunsnlem  15401  coprmprod  15422  coprmproddvds  15424  isprs  16977  drsdirfi  16985  isdrs2  16986  ispos  16994  lubeldm  17028  lubval  17031  glbeldm  17041  glbval  17044  istos  17082  pospropd  17181  isdlat  17240  mhmpropd  17388  isghm  17707  cntzval  17800  efgval  18176  iscmn  18246  dfrhm2  18765  lidldvgen  19303  coe1fzgsumd  19720  evl1gsumd  19769  ocvval  20059  isobs  20112  mat0dimcrng  20324  mdetunilem9  20474  ist0  21172  cmpcovf  21242  is1stc  21292  2ndc1stc  21302  isref  21360  txflf  21857  ustuqtop4  22095  iscfilu  22139  ispsmet  22156  ismet  22175  isxmet  22176  cncfval  22738  lebnumlem3  22809  fmcfil  23116  iscfil3  23117  caucfil  23127  iscmet3  23137  cfilres  23140  minveclem3  23246  ovolfiniun  23315  finiunmbl  23358  volfiniun  23361  dvcn  23729  ulmval  24179  axtgcont1  25412  tgcgr4  25471  nb3grpr  26328  prcliscplgr  26365  dfconngr1  27166  isconngr  27167  1conngr  27172  frgr0v  27241  isplig  27458  isgrpo  27479  isablo  27528  ocval  28267  acunirnmpt  29587  isomnd  29829  isorng  29927  ismbfm  30442  isanmbfm  30446  bnj865  31119  bnj1154  31193  bnj1296  31215  bnj1463  31249  derangval  31275  setinds  31807  dfon2lem3  31814  dfon2lem7  31818  tfisg  31840  poseq  31878  frrlem1  31905  sltval2  31934  sltres  31940  nolesgn2o  31949  nodense  31967  nosupbnd2lem1  31986  brsslt  32025  dfrecs2  32182  dfrdg4  32183  isfne  32459  finixpnum  33524  mblfinlem1  33576  mbfresfi  33586  indexdom  33659  heibor1lem  33738  isexid2  33784  ismndo2  33803  rngomndo  33864  pridl  33966  smprngopr  33981  ispridlc  33999  setindtrs  37909  dford3lem2  37911  dfac11  37949  fnchoice  39502  axccdom  39730  axccd  39743  stoweidlem31  40566  stoweidlem57  40592  fourierdlem80  40721  fourierdlem103  40744  fourierdlem104  40745  isvonmbl  41173  mgmhmpropd  42110  rnghmval  42216  zrrnghm  42242  bnd2d  42753