Theorem raleq 3343

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-ral 3070

This theorem is referenced by:  raleqi  3347  raleqdv  3349  sbralie  3407  r19.2zb  4427  inteq  4883  iineq1  4942  friOLD  5551  frsn  5675  fncnv  6514  isoeq4  7200  onminex  7661  tfinds  7715  f1oweALT  7824  frxp  7976  frrlem1  8111  frrlem13  8123  wfrlem1OLD  8148  wfrlem15OLD  8163  tfrlem1  8216  tfrlem12  8229  omeulem1  8422  ixpeq1  8705  undifixp  8731  ac6sfi  9067  frfi  9068  iunfi  9116  indexfi  9136  supeq1  9213  supeq2  9216  brttrcl2  9481  ssttrcl  9482  ttrcltr  9483  bnd2  9660  acneq  9808  aceq3lem  9885  dfac5lem4  9891  dfac8  9900  dfac9  9901  kmlem1  9915  kmlem10  9924  kmlem13  9927  cfval  10012  axcc2lem  10201  axcc4dom  10206  axdc3lem3  10217  axdc3lem4  10218  ac4c  10241  ac5  10242  ac6sg  10253  zorn2lem7  10267  xrsupsslem  13050  xrinfmsslem  13051  xrsupss  13052  xrinfmss  13053  fsuppmapnn0fiubex  13721  rexanuz  15066  rexfiuz  15068  modfsummod  15515  gcdcllem3  16217  lcmfval  16335  lcmf0val  16336  lcmfunsnlem  16355  coprmprod  16375  coprmproddvds  16377  isprs  18024  drsdirfi  18032  isdrs2  18033  ispos  18041  pospropd  18054  lubeldm  18080  lubval  18083  glbeldm  18093  glbval  18096  istos  18145  isdlat  18249  mhmpropd  18445  isghm  18843  cntzval  18936  efgval  19332  iscmn  19403  dfrhm2  19970  lidldvgen  20535  ocvval  20881  isobs  20936  coe1fzgsumd  21482  evl1gsumd  21532  mat0dimcrng  21628  mdetunilem9  21778  ist0  22480  cmpcovf  22551  is1stc  22601  2ndc1stc  22611  isref  22669  txflf  23166  ustuqtop4  23405  iscfilu  23449  ispsmet  23466  ismet  23485  isxmet  23486  cncfval  24060  lebnumlem3  24135  fmcfil  24445  iscfil3  24446  caucfil  24456  iscmet3  24466  cfilres  24469  minveclem3  24602  ovolfiniun  24674  finiunmbl  24717  volfiniun  24720  dvcn  25094  ulmval  25548  axtgcont1  26838  nb3grpr  27758  dfconngr1  28561  isconngr  28562  1conngr  28567  frgr0v  28635  isplig  28847  isgrpo  28868  isablo  28917  ocval  29651  acunirnmpt  31005  isomnd  31336  isorng  31507  prmidl  31624  ismbfm  32228  isanmbfm  32232  bnj865  32912  bnj1154  32988  bnj1296  33010  bnj1463  33044  derangval  33138  setinds  33763  dfon2lem3  33770  dfon2lem7  33774  tfisg  33795  frxp2  33800  frxp3  33806  poseq  33811  sltval2  33868  sltres  33874  nolesgn2o  33883  nogesgn1o  33885  nodense  33904  nosupbnd2lem1  33927  noinfbnd2lem1  33942  brsslt  33989  madebday  34089  dfrecs2  34261  dfrdg4  34262  isfne  34537  finixpnum  35771  mblfinlem1  35823  mbfresfi  35832  indexdom  35901  heibor1lem  35976  isexid2  36022  ismndo2  36041  rngomndo  36102  pridl  36204  smprngopr  36219  ispridlc  36237  setindtrs  40854  dford3lem2  40856  dfac11  40894  mnuop123d  41887  fnchoice  42579  axccdom  42769  axccd  42775  stoweidlem31  43579  stoweidlem57  43605  fourierdlem80  43734  fourierdlem103  43757  fourierdlem104  43758  isvonmbl  44183  paireqne  44974  requad2  45086  mgmhmpropd  45350  rnghmval  45460  zrrnghm  45486  isthinc  46313  0thincg  46342  bnd2d  46398