Theorem raleqbi1dv 3335

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (Proof shortened by Steven Nguyen, 5-May-2023.)

Hypothesis

Ref	Expression
raleqbi1dv.1	⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem raleqbi1dv

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		raleqbi1dv.1	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))
3	1, 2	raleqbidvv 3331	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ral 3059  df-rex 3068

This theorem is referenced by:  raleqOLD  3337  isoeq4  7339  frrlem1  8309  frrlem13  8321  wfrlem1OLD  8346  wfrlem4OLD  8350  wfrlem15OLD  8361  smo11  8402  dffi2  9460  inficl  9462  dffi3  9468  dfom3  9684  aceq1  10154  dfac5lem4  10163  dfac5lem4OLD  10165  kmlem1  10188  kmlem10  10197  kmlem13  10200  kmlem14  10201  cofsmo  10306  infpssrlem4  10343  axdc3lem2  10488  elwina  10723  elina  10724  iswun  10741  eltskg  10787  elgrug  10829  elnp  11024  elnpi  11025  dfnn2  12276  dfnn3  12277  dfuzi  12706  coprmprod  16694  coprmproddvds  16696  ismri  17675  isprs  18353  isdrs  18358  ispos  18371  pospropd  18384  istos  18475  isdlat  18579  isipodrs  18594  mgmhmpropd  18723  issubmgm  18727  mhmpropd  18817  issubm  18828  subgacs  19191  nsgacs  19192  isghm  19245  isghmOLD  19246  ghmeql  19269  iscmn  19821  rnghmval  20456  dfrhm2  20490  zrrnghm  20552  islss  20949  lssacs  20982  lmhmeql  21071  islbs  21092  lbsextlem1  21177  lbsextlem3  21179  lbsextlem4  21180  isobs  21757  mat0dimcrng  22491  istopg  22916  isbasisg  22969  basis2  22973  eltg2  22980  iscldtop  23118  neipeltop  23152  isreg  23355  regsep  23357  isnrm  23358  islly  23491  isnlly  23492  llyi  23497  nllyi  23498  islly2  23507  cldllycmp  23518  isfbas  23852  fbssfi  23860  isust  24227  elutop  24257  ustuqtop  24270  utopsnneip  24272  ispsmet  24329  ismet  24348  isxmet  24349  metrest  24552  cncfval  24927  fmcfil  25319  iscfil3  25320  caucfil  25330  iscmet3  25340  cfilres  25343  minveclem3  25476  wilthlem2  27126  wilthlem3  27127  wilth  27128  dfn0s2  28350  dfconngr1  30216  isconngr  30217  1conngr  30222  isplig  30504  isgrpo  30525  isablo  30574  disjabrex  32601  disjabrexf  32602  isomnd  33060  isorng  33308  isrnsiga  34093  isldsys  34136  isros  34148  issros  34155  bnj1286  35011  bnj1452  35044  kur14lem9  35198  cvmscbv  35242  cvmsi  35249  cvmsval  35250  neibastop1  36341  neibastop2lem  36342  neibastop2  36343  rdgssun  37360  isbnd  37766  ismndo2  37860  rngomndo  37921  isidl  38000  ispsubsp  39727  sn-isghm  42659  isnacs  42691  mzpclval  42712  elmzpcl  42713  isthinc  48820