Theorem raleq 3333

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ral 3068

This theorem is referenced by:  raleqi  3337  raleqdv  3339  sbralie  3395  r19.2zb  4423  inteq  4879  iineq1  4938  friOLD  5541  frsn  5665  fncnv  6491  isoeq4  7171  onminex  7629  tfinds  7681  f1oweALT  7788  frxp  7938  frrlem1  8073  frrlem13  8085  wfrlem1OLD  8110  wfrlem15OLD  8125  tfrlem1  8178  tfrlem12  8191  omeulem1  8375  ixpeq1  8654  undifixp  8680  ac6sfi  8988  frfi  8989  iunfi  9037  indexfi  9057  supeq1  9134  supeq2  9137  bnd2  9582  acneq  9730  aceq3lem  9807  dfac5lem4  9813  dfac8  9822  dfac9  9823  kmlem1  9837  kmlem10  9846  kmlem13  9849  cfval  9934  axcc2lem  10123  axcc4dom  10128  axdc3lem3  10139  axdc3lem4  10140  ac4c  10163  ac5  10164  ac6sg  10175  zorn2lem7  10189  xrsupsslem  12970  xrinfmsslem  12971  xrsupss  12972  xrinfmss  12973  fsuppmapnn0fiubex  13640  rexanuz  14985  rexfiuz  14987  modfsummod  15434  gcdcllem3  16136  lcmfval  16254  lcmf0val  16255  lcmfunsnlem  16274  coprmprod  16294  coprmproddvds  16296  isprs  17930  drsdirfi  17938  isdrs2  17939  ispos  17947  pospropd  17960  lubeldm  17986  lubval  17989  glbeldm  17999  glbval  18002  istos  18051  isdlat  18155  mhmpropd  18351  isghm  18749  cntzval  18842  efgval  19238  iscmn  19309  dfrhm2  19876  lidldvgen  20439  ocvval  20784  isobs  20837  coe1fzgsumd  21383  evl1gsumd  21433  mat0dimcrng  21527  mdetunilem9  21677  ist0  22379  cmpcovf  22450  is1stc  22500  2ndc1stc  22510  isref  22568  txflf  23065  ustuqtop4  23304  iscfilu  23348  ispsmet  23365  ismet  23384  isxmet  23385  cncfval  23957  lebnumlem3  24032  fmcfil  24341  iscfil3  24342  caucfil  24352  iscmet3  24362  cfilres  24365  minveclem3  24498  ovolfiniun  24570  finiunmbl  24613  volfiniun  24616  dvcn  24990  ulmval  25444  axtgcont1  26733  nb3grpr  27652  dfconngr1  28453  isconngr  28454  1conngr  28459  frgr0v  28527  isplig  28739  isgrpo  28760  isablo  28809  ocval  29543  acunirnmpt  30898  isomnd  31229  isorng  31400  prmidl  31517  ismbfm  32119  isanmbfm  32123  bnj865  32803  bnj1154  32879  bnj1296  32901  bnj1463  32935  derangval  33029  setinds  33660  dfon2lem3  33667  dfon2lem7  33671  tfisg  33692  brttrcl2  33700  ssttrcl  33701  ttrcltr  33702  frxp2  33718  frxp3  33724  poseq  33729  sltval2  33786  sltres  33792  nolesgn2o  33801  nogesgn1o  33803  nodense  33822  nosupbnd2lem1  33845  noinfbnd2lem1  33860  brsslt  33907  madebday  34007  dfrecs2  34179  dfrdg4  34180  isfne  34455  finixpnum  35689  mblfinlem1  35741  mbfresfi  35750  indexdom  35819  heibor1lem  35894  isexid2  35940  ismndo2  35959  rngomndo  36020  pridl  36122  smprngopr  36137  ispridlc  36155  setindtrs  40763  dford3lem2  40765  dfac11  40803  mnuop123d  41769  fnchoice  42461  axccdom  42651  axccd  42657  stoweidlem31  43462  stoweidlem57  43488  fourierdlem80  43617  fourierdlem103  43640  fourierdlem104  43641  isvonmbl  44066  paireqne  44851  requad2  44963  mgmhmpropd  45227  rnghmval  45337  zrrnghm  45363  isthinc  46190  0thincg  46219  bnd2d  46273