Theorem raleq 3114

Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleq

Step	Hyp	Ref	Expression
1		nfcv 2750	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2750	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	raleqf 3110	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 194   = wceq 1474  ∀wral 2895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900

This theorem is referenced by:  raleqi  3118  raleqdv  3120  raleqbi1dv  3122  sbralie  3159  r19.2zb  4012  inteq  4407  iineq1  4465  fri  4990  frsn  5102  fncnv  5862  isoeq4  6448  onminex  6876  tfinds  6928  f1oweALT  7020  frxp  7151  wfrlem1  7278  wfrlem15  7293  tfrlem1  7336  tfrlem12  7349  omeulem1  7526  ixpeq1  7782  undifixp  7807  ac6sfi  8066  frfi  8067  iunfi  8114  indexfi  8134  supeq1  8211  supeq2  8214  bnd2  8616  acneq  8726  aceq3lem  8803  dfac5lem4  8809  dfac8  8817  dfac9  8818  kmlem1  8832  kmlem10  8841  kmlem13  8844  cfval  8929  axcc2lem  9118  axcc4dom  9123  axdc3lem3  9134  axdc3lem4  9135  ac4c  9158  ac5  9159  ac6sg  9170  zorn2lem7  9184  xrsupsslem  11965  xrinfmsslem  11966  xrsupss  11967  xrinfmss  11968  fsuppmapnn0fiubex  12609  rexanuz  13879  rexfiuz  13881  modfsummod  14313  gcdcllem3  15007  lcmfval  15118  lcmf0val  15119  lcmfunsnlem  15138  coprmprod  15159  coprmproddvds  15161  isprs  16699  drsdirfi  16707  isdrs2  16708  ispos  16716  lubeldm  16750  lubval  16753  glbeldm  16763  glbval  16766  istos  16804  pospropd  16903  isdlat  16962  mgm0  17024  sgrp0  17060  mhmpropd  17110  isghm  17429  cntzval  17523  efgval  17899  iscmn  17969  dfrhm2  18486  lidldvgen  19022  coe1fzgsumd  19439  evl1gsumd  19488  ocvval  19772  isobs  19825  mat0dimcrng  20037  mdetunilem9  20187  ist0  20876  cmpcovf  20946  is1stc  20996  2ndc1stc  21006  isref  21064  txflf  21562  ustuqtop4  21800  iscfilu  21844  ispsmet  21861  ismet  21879  isxmet  21880  cncfval  22430  lebnumlem3  22501  fmcfil  22796  iscfil3  22797  caucfil  22807  iscmet3  22817  cfilres  22820  minveclem3  22925  ovolfiniun  22993  finiunmbl  23036  volfiniun  23039  dvcn  23407  ulmval  23855  axtgcont1  25084  tgcgr4  25144  nb3grapr  25748  rusgrasn  26238  isplig  26486  isgrpo  26501  isablo  26553  ocval  27329  acunirnmpt  28647  isomnd  28838  isorng  28936  ismbfm  29447  isanmbfm  29451  bnj865  30053  bnj1154  30127  bnj1296  30149  bnj1463  30183  derangval  30209  setinds  30733  dfon2lem3  30740  dfon2lem7  30744  tfisg  30766  poseq  30800  frrlem1  30830  sltval2  30859  sltres  30867  nodense  30894  nobndup  30905  nobnddown  30906  nofulllem1  30907  dfrecs2  31033  dfrdg4  31034  isfne  31310  finixpnum  32360  mblfinlem1  32412  mbfresfi  32422  indexdom  32495  heibor1lem  32574  isexid2  32620  ismndo2  32639  rngomndo  32700  pridl  32802  smprngopr  32817  ispridlc  32835  setindtrs  36406  dford3lem2  36408  dfac11  36446  fnchoice  38007  axccdom  38207  axccd  38220  stoweidlem31  38721  stoweidlem57  38747  fourierdlem80  38876  fourierdlem103  38899  fourierdlem104  38900  issal  39007  isvonmbl  39325  nb3grpr  40605  cplgr0v  40644  dfconngr1  41350  isconngr  41351  0vconngr  41355  1conngr  41356  frgr0v  41428  mgmhmpropd  41570  rnghmval  41676  zrrnghm  41702