Theorem raleq 3338

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 2959	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2959	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	raleqf 3334	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  ∀wral 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112

This theorem is referenced by:  raleqi  3342  raleqdv  3344  raleqbi1dv  3346  sbralie  3384  r19.2zb  4267  inteq  4683  iineq1  4738  fri  5286  frsn  5404  fncnv  6182  isoeq4  6803  onminex  7246  tfinds  7298  f1oweALT  7391  frxp  7530  wfrlem1  7658  wfrlem15  7674  tfrlem1  7717  tfrlem12  7730  omeulem1  7908  ixpeq1  8165  undifixp  8190  ac6sfi  8452  frfi  8453  iunfi  8502  indexfi  8522  supeq1  8599  supeq2  8602  bnd2  9012  acneq  9158  aceq3lem  9235  dfac5lem4  9241  dfac8  9251  dfac9  9252  kmlem1  9266  kmlem10  9275  kmlem13  9278  cfval  9363  axcc2lem  9552  axcc4dom  9557  axdc3lem3  9568  axdc3lem4  9569  ac4c  9592  ac5  9593  ac6sg  9604  zorn2lem7  9618  xrsupsslem  12374  xrinfmsslem  12375  xrsupss  12376  xrinfmss  12377  fsuppmapnn0fiubex  13034  rexanuz  14327  rexfiuz  14329  modfsummod  14767  gcdcllem3  15461  lcmfval  15572  lcmf0val  15573  lcmfunsnlem  15592  coprmprod  15612  coprmproddvds  15614  isprs  17154  drsdirfi  17162  isdrs2  17163  ispos  17171  lubeldm  17205  lubval  17208  glbeldm  17218  glbval  17221  istos  17259  pospropd  17358  isdlat  17417  mhmpropd  17565  isghm  17881  cntzval  17974  efgval  18350  iscmn  18420  dfrhm2  18940  lidldvgen  19483  coe1fzgsumd  19899  evl1gsumd  19948  ocvval  20241  isobs  20294  mat0dimcrng  20507  mdetunilem9  20657  ist0  21358  cmpcovf  21428  is1stc  21478  2ndc1stc  21488  isref  21546  txflf  22043  ustuqtop4  22281  iscfilu  22325  ispsmet  22342  ismet  22361  isxmet  22362  cncfval  22924  lebnumlem3  22995  fmcfil  23303  iscfil3  23304  caucfil  23314  iscmet3  23324  cfilres  23327  minveclem3  23434  ovolfiniun  23504  finiunmbl  23547  volfiniun  23550  dvcn  23920  ulmval  24370  axtgcont1  25603  tgcgr4  25662  nb3grpr  26522  prcliscplgr  26559  dfconngr1  27383  isconngr  27384  1conngr  27389  frgr0v  27458  isplig  27681  isgrpo  27702  isablo  27751  ocval  28489  acunirnmpt  29808  isomnd  30048  isorng  30146  ismbfm  30661  isanmbfm  30665  bnj865  31337  bnj1154  31411  bnj1296  31433  bnj1463  31467  derangval  31493  setinds  32024  dfon2lem3  32031  dfon2lem7  32035  tfisg  32057  poseq  32095  frrlem1  32122  sltval2  32151  sltres  32157  nolesgn2o  32166  nodense  32184  nosupbnd2lem1  32203  brsslt  32242  dfrecs2  32399  dfrdg4  32400  isfne  32676  finixpnum  33725  mblfinlem1  33777  mbfresfi  33786  indexdom  33859  heibor1lem  33937  isexid2  33983  ismndo2  34002  rngomndo  34063  pridl  34165  smprngopr  34180  ispridlc  34198  setindtrs  38110  dford3lem2  38112  dfac11  38150  fnchoice  39699  axccdom  39920  axccd  39930  stoweidlem31  40744  stoweidlem57  40770  fourierdlem80  40899  fourierdlem103  40922  fourierdlem104  40923  isvonmbl  41351  mgmhmpropd  42370  rnghmval  42476  zrrnghm  42502  bnd2d  43013