Theorem raleqbi1dv 3308

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 3304	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ral 3045  df-rex 3054

This theorem is referenced by:  raleqOLD  3310  isoeq4  7277  frrlem1  8242  frrlem13  8254  smo11  8310  dffi2  9350  inficl  9352  dffi3  9358  dfom3  9576  aceq1  10046  dfac5lem4  10055  dfac5lem4OLD  10057  kmlem1  10080  kmlem10  10089  kmlem13  10092  kmlem14  10093  cofsmo  10198  infpssrlem4  10235  axdc3lem2  10380  elwina  10615  elina  10616  iswun  10633  eltskg  10679  elgrug  10721  elnp  10916  elnpi  10917  dfnn2  12175  dfnn3  12176  dfuzi  12601  coprmprod  16607  coprmproddvds  16609  ismri  17572  isprs  18237  isdrs  18242  ispos  18255  pospropd  18266  istos  18357  isdlat  18463  isipodrs  18478  mgmhmpropd  18607  issubmgm  18611  mhmpropd  18701  issubm  18712  subgacs  19075  nsgacs  19076  isghm  19129  isghmOLD  19130  ghmeql  19153  iscmn  19703  isomnd  20037  rnghmval  20360  dfrhm2  20394  zrrnghm  20456  isorng  20781  islss  20872  lssacs  20905  lmhmeql  20994  islbs  21015  lbsextlem1  21100  lbsextlem3  21102  lbsextlem4  21103  isobs  21662  mat0dimcrng  22390  istopg  22815  isbasisg  22867  basis2  22871  eltg2  22878  iscldtop  23015  neipeltop  23049  isreg  23252  regsep  23254  isnrm  23255  islly  23388  isnlly  23389  llyi  23394  nllyi  23395  islly2  23404  cldllycmp  23415  isfbas  23749  fbssfi  23757  isust  24124  elutop  24154  ustuqtop  24167  utopsnneip  24169  ispsmet  24225  ismet  24244  isxmet  24245  metrest  24445  cncfval  24814  fmcfil  25205  iscfil3  25206  caucfil  25216  iscmet3  25226  cfilres  25229  minveclem3  25362  wilthlem2  27012  wilthlem3  27013  wilth  27014  dfn0s2  28264  dfconngr1  30167  isconngr  30168  1conngr  30173  isplig  30455  isgrpo  30476  isablo  30525  disjabrex  32561  disjabrexf  32562  isrnsiga  34096  isldsys  34139  isros  34151  issros  34158  bnj1286  35002  bnj1452  35035  kur14lem9  35194  cvmscbv  35238  cvmsi  35245  cvmsval  35246  neibastop1  36340  neibastop2lem  36341  neibastop2  36342  rdgssun  37359  isbnd  37767  ismndo2  37861  rngomndo  37922  isidl  38001  ispsubsp  39732  sn-isghm  42654  isnacs  42685  mzpclval  42706  elmzpcl  42707  relpeq4  44930  permac8prim  44997  nelsubc3lem  49052  isthinc  49401