Theorem raleq 3307

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-ral 3061

This theorem is referenced by:  raleqi  3309  raleqdv  3311  sbralie  3330  r19.2zb  4458  inteq  4915  iineq1  4976  friOLD  5599  frsn  5724  fncnv  6579  isoeq4  7270  onminex  7742  tfisg  7795  tfinds  7801  f1oweALT  7910  frxp  8063  frxp2  8081  poseq  8095  frrlem1  8222  frrlem13  8234  wfrlem1OLD  8259  wfrlem15OLD  8274  tfrlem1  8327  tfrlem12  8340  omeulem1  8534  ixpeq1  8853  undifixp  8879  ac6sfi  9238  frfi  9239  iunfi  9291  indexfi  9311  supeq1  9390  supeq2  9393  brttrcl2  9659  ssttrcl  9660  ttrcltr  9661  bnd2  9838  acneq  9988  aceq3lem  10065  dfac5lem4  10071  dfac8  10080  dfac9  10081  kmlem1  10095  kmlem10  10104  kmlem13  10107  cfval  10192  axcc2lem  10381  axcc4dom  10386  axdc3lem3  10397  axdc3lem4  10398  ac4c  10421  ac5  10422  ac6sg  10433  zorn2lem7  10447  xrsupsslem  13236  xrinfmsslem  13237  xrsupss  13238  xrinfmss  13239  fsuppmapnn0fiubex  13907  rexanuz  15242  rexfiuz  15244  modfsummod  15690  gcdcllem3  16392  lcmfval  16508  lcmf0val  16509  lcmfunsnlem  16528  coprmprod  16548  coprmproddvds  16550  isprs  18200  drsdirfi  18208  isdrs2  18209  ispos  18217  pospropd  18230  lubeldm  18256  lubval  18259  glbeldm  18269  glbval  18272  istos  18321  isdlat  18425  mhmpropd  18622  isghm  19022  cntzval  19115  efgval  19513  iscmn  19585  dfrhm2  20164  lidldvgen  20784  ocvval  21108  isobs  21163  coe1fzgsumd  21710  evl1gsumd  21760  mat0dimcrng  21856  mdetunilem9  22006  ist0  22708  cmpcovf  22779  is1stc  22829  2ndc1stc  22839  isref  22897  txflf  23394  ustuqtop4  23633  iscfilu  23677  ispsmet  23694  ismet  23713  isxmet  23714  cncfval  24288  lebnumlem3  24363  fmcfil  24673  iscfil3  24674  caucfil  24684  iscmet3  24694  cfilres  24697  minveclem3  24830  ovolfiniun  24902  finiunmbl  24945  volfiniun  24948  dvcn  25322  ulmval  25776  sltval2  27041  sltres  27047  nolesgn2o  27056  nogesgn1o  27058  nodense  27077  nosupbnd2lem1  27100  noinfbnd2lem1  27115  brsslt  27168  madebday  27272  negsprop  27376  axtgcont1  27473  nb3grpr  28393  dfconngr1  29195  isconngr  29196  1conngr  29201  frgr0v  29269  isplig  29481  isgrpo  29502  isablo  29551  ocval  30285  acunirnmpt  31642  isomnd  31979  isorng  32165  prmidl  32288  ismbfm  32939  bnj865  33624  bnj1154  33700  bnj1296  33722  bnj1463  33756  derangval  33848  setinds  34439  dfon2lem3  34446  dfon2lem7  34450  dfrecs2  34611  dfrdg4  34612  isfne  34887  finixpnum  36136  mblfinlem1  36188  mbfresfi  36197  indexdom  36266  heibor1lem  36341  isexid2  36387  ismndo2  36406  rngomndo  36467  pridl  36569  smprngopr  36584  ispridlc  36602  setindtrs  41407  dford3lem2  41409  dfac11  41447  rp-intrabeq  41613  rp-unirabeq  41614  rp-brsslt  41817  mnuop123d  42664  fnchoice  43356  axccdom  43564  axccd  43571  stoweidlem31  44392  stoweidlem57  44418  fourierdlem80  44547  fourierdlem103  44570  fourierdlem104  44571  isvonmbl  44999  paireqne  45823  requad2  45935  mgmhmpropd  46199  rnghmval  46309  zrrnghm  46335  isthinc  47161  0thincg  47190  bnd2d  47246