Theorem raleq 3309

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2143, ax-11 2160, and ax-12 2177. (Revised by Steven Nguyen, 30-Apr-2023.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleq

Step	Hyp	Ref	Expression
1		biidd 265	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜑))
2	1	raleqbi1dv 3307	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-ral 3056

This theorem is referenced by:  raleqi  3313  raleqdv  3315  sbralie  3371  r19.2zb  4393  inteq  4848  iineq1  4907  fri  5497  frsn  5621  fncnv  6431  isoeq4  7107  onminex  7564  tfinds  7616  f1oweALT  7723  frxp  7871  frrlem1  8005  frrlem13  8017  wfrlem1  8032  wfrlem15  8047  tfrlem1  8090  tfrlem12  8103  omeulem1  8288  ixpeq1  8567  undifixp  8593  ac6sfi  8893  frfi  8894  iunfi  8942  indexfi  8962  supeq1  9039  supeq2  9042  bnd2  9474  acneq  9622  aceq3lem  9699  dfac5lem4  9705  dfac8  9714  dfac9  9715  kmlem1  9729  kmlem10  9738  kmlem13  9741  cfval  9826  axcc2lem  10015  axcc4dom  10020  axdc3lem3  10031  axdc3lem4  10032  ac4c  10055  ac5  10056  ac6sg  10067  zorn2lem7  10081  xrsupsslem  12862  xrinfmsslem  12863  xrsupss  12864  xrinfmss  12865  fsuppmapnn0fiubex  13530  rexanuz  14874  rexfiuz  14876  modfsummod  15321  gcdcllem3  16023  lcmfval  16141  lcmf0val  16142  lcmfunsnlem  16161  coprmprod  16181  coprmproddvds  16183  isprs  17758  drsdirfi  17766  isdrs2  17767  ispos  17775  pospropd  17787  lubeldm  17813  lubval  17816  glbeldm  17826  glbval  17829  istos  17878  isdlat  17982  mhmpropd  18178  isghm  18576  cntzval  18669  efgval  19061  iscmn  19132  dfrhm2  19691  lidldvgen  20247  ocvval  20583  isobs  20636  coe1fzgsumd  21177  evl1gsumd  21227  mat0dimcrng  21321  mdetunilem9  21471  ist0  22171  cmpcovf  22242  is1stc  22292  2ndc1stc  22302  isref  22360  txflf  22857  ustuqtop4  23096  iscfilu  23139  ispsmet  23156  ismet  23175  isxmet  23176  cncfval  23739  lebnumlem3  23814  fmcfil  24123  iscfil3  24124  caucfil  24134  iscmet3  24144  cfilres  24147  minveclem3  24280  ovolfiniun  24352  finiunmbl  24395  volfiniun  24398  dvcn  24772  ulmval  25226  axtgcont1  26513  nb3grpr  27424  dfconngr1  28225  isconngr  28226  1conngr  28231  frgr0v  28299  isplig  28511  isgrpo  28532  isablo  28581  ocval  29315  acunirnmpt  30670  isomnd  31000  isorng  31171  prmidl  31283  ismbfm  31885  isanmbfm  31889  bnj865  32570  bnj1154  32646  bnj1296  32668  bnj1463  32702  derangval  32796  setinds  33424  dfon2lem3  33431  dfon2lem7  33435  tfisg  33456  frxp2  33471  frxp3  33477  poseq  33482  sltval2  33545  sltres  33551  nolesgn2o  33560  nogesgn1o  33562  nodense  33581  nosupbnd2lem1  33604  noinfbnd2lem1  33619  brsslt  33666  madebday  33766  dfrecs2  33938  dfrdg4  33939  isfne  34214  finixpnum  35448  mblfinlem1  35500  mbfresfi  35509  indexdom  35578  heibor1lem  35653  isexid2  35699  ismndo2  35718  rngomndo  35779  pridl  35881  smprngopr  35896  ispridlc  35914  setindtrs  40491  dford3lem2  40493  dfac11  40531  mnuop123d  41494  fnchoice  42186  axccdom  42376  axccd  42382  stoweidlem31  43190  stoweidlem57  43216  fourierdlem80  43345  fourierdlem103  43368  fourierdlem104  43369  isvonmbl  43794  paireqne  44579  requad2  44691  mgmhmpropd  44955  rnghmval  45065  zrrnghm  45091  isthinc  45918  0thincg  45947  bnd2d  46001