Theorem raleq 3339

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2079, ax-11 2093, and ax-12 2106. (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 254	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜑))
2	1	raleqbi1dv 3337	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507  ∀wral 3082

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-clel 2840  df-ral 3087

This theorem is referenced by:  raleqi  3347  raleqdv  3349  raleqbi1dvOLD  3351  sbralie  3391  r19.2zb  4318  inteq  4748  iineq1  4804  fri  5365  frsn  5485  fncnv  6257  isoeq4  6894  onminex  7336  tfinds  7388  f1oweALT  7483  frxp  7623  wfrlem1  7755  wfrlem15  7771  tfrlem1  7814  tfrlem12  7827  omeulem1  8007  ixpeq1  8268  undifixp  8293  ac6sfi  8555  frfi  8556  iunfi  8605  indexfi  8625  supeq1  8702  supeq2  8705  bnd2  9114  acneq  9261  aceq3lem  9338  dfac5lem4  9344  dfac8  9353  dfac9  9354  kmlem1  9368  kmlem10  9377  kmlem13  9380  cfval  9465  axcc2lem  9654  axcc4dom  9659  axdc3lem3  9670  axdc3lem4  9671  ac4c  9694  ac5  9695  ac6sg  9706  zorn2lem7  9720  xrsupsslem  12514  xrinfmsslem  12515  xrsupss  12516  xrinfmss  12517  fsuppmapnn0fiubex  13173  rexanuz  14564  rexfiuz  14566  modfsummod  15007  gcdcllem3  15708  lcmfval  15819  lcmf0val  15820  lcmfunsnlem  15839  coprmprod  15859  coprmproddvds  15861  isprs  17410  drsdirfi  17418  isdrs2  17419  ispos  17427  lubeldm  17461  lubval  17464  glbeldm  17474  glbval  17477  istos  17515  pospropd  17614  isdlat  17673  mhmpropd  17821  isghm  18141  cntzval  18234  efgval  18613  iscmn  18685  dfrhm2  19204  lidldvgen  19761  coe1fzgsumd  20185  evl1gsumd  20234  ocvval  20525  isobs  20578  mat0dimcrng  20795  mdetunilem9  20945  ist0  21644  cmpcovf  21715  is1stc  21765  2ndc1stc  21775  isref  21833  txflf  22330  ustuqtop4  22568  iscfilu  22612  ispsmet  22629  ismet  22648  isxmet  22649  cncfval  23211  lebnumlem3  23282  fmcfil  23590  iscfil3  23591  caucfil  23601  iscmet3  23611  cfilres  23614  minveclem3  23747  ovolfiniun  23817  finiunmbl  23860  volfiniun  23863  dvcn  24233  ulmval  24683  axtgcont1  25968  tgcgr4  26031  nb3grpr  26879  dfconngr1  27729  isconngr  27730  1conngr  27735  frgr0v  27807  isplig  28042  isgrpo  28063  isablo  28112  ocval  28850  acunirnmpt  30180  isomnd  30443  isorng  30580  ismbfm  31184  isanmbfm  31188  bnj865  31871  bnj1154  31945  bnj1296  31967  bnj1463  32001  derangval  32028  setinds  32572  dfon2lem3  32579  dfon2lem7  32583  tfisg  32605  poseq  32645  frrlem1  32673  frrlem13  32685  sltval2  32713  sltres  32719  nolesgn2o  32728  nodense  32746  nosupbnd2lem1  32765  brsslt  32804  dfrecs2  32961  dfrdg4  32962  isfne  33237  finixpnum  34347  mblfinlem1  34399  mbfresfi  34408  indexdom  34480  heibor1lem  34558  isexid2  34604  ismndo2  34623  rngomndo  34684  pridl  34786  smprngopr  34801  ispridlc  34819  setindtrs  39047  dford3lem2  39049  dfac11  39087  mnuop123d  40002  fnchoice  40734  axccdom  40938  axccd  40947  stoweidlem31  41772  stoweidlem57  41798  fourierdlem80  41927  fourierdlem103  41950  fourierdlem104  41951  isvonmbl  42376  paireqne  43066  requad2  43181  mgmhmpropd  43445  rnghmval  43551  zrrnghm  43577  bnd2d  44176