Theorem raleqbi1dv 3306

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

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

This theorem is referenced by:  raleqOLD  3308  isoeq4  7264  frrlem1  8226  frrlem13  8238  smo11  8294  dffi2  9324  inficl  9326  dffi3  9332  dfom3  9554  aceq1  10025  dfac5lem4  10034  dfac5lem4OLD  10036  kmlem1  10059  kmlem10  10068  kmlem13  10071  kmlem14  10072  cofsmo  10177  infpssrlem4  10214  axdc3lem2  10359  elwina  10595  elina  10596  iswun  10613  eltskg  10659  elgrug  10701  elnp  10896  elnpi  10897  dfnn2  12156  dfnn3  12157  dfuzi  12581  coprmprod  16586  coprmproddvds  16588  ismri  17552  isprs  18217  isdrs  18222  ispos  18235  pospropd  18246  istos  18337  isdlat  18443  isipodrs  18458  mgmhmpropd  18621  issubmgm  18625  mhmpropd  18715  issubm  18726  subgacs  19088  nsgacs  19089  isghm  19142  isghmOLD  19143  ghmeql  19166  iscmn  19716  isomnd  20050  rnghmval  20374  dfrhm2  20408  zrrnghm  20467  isorng  20792  islss  20883  lssacs  20916  lmhmeql  21005  islbs  21026  lbsextlem1  21111  lbsextlem3  21113  lbsextlem4  21114  isobs  21673  mat0dimcrng  22412  istopg  22837  isbasisg  22889  basis2  22893  eltg2  22900  iscldtop  23037  neipeltop  23071  isreg  23274  regsep  23276  isnrm  23277  islly  23410  isnlly  23411  llyi  23416  nllyi  23417  islly2  23426  cldllycmp  23437  isfbas  23771  fbssfi  23779  isust  24146  elutop  24175  ustuqtop  24188  utopsnneip  24190  ispsmet  24246  ismet  24265  isxmet  24266  metrest  24466  cncfval  24835  fmcfil  25226  iscfil3  25227  caucfil  25237  iscmet3  25247  cfilres  25250  minveclem3  25383  wilthlem2  27033  wilthlem3  27034  wilth  27035  dfn0s2  28292  dfconngr1  30212  isconngr  30213  1conngr  30218  isplig  30500  isgrpo  30521  isablo  30570  disjabrex  32606  disjabrexf  32607  isrnsiga  34219  isldsys  34262  isros  34274  issros  34281  bnj1286  35124  bnj1452  35157  kur14lem9  35357  cvmscbv  35401  cvmsi  35408  cvmsval  35409  neibastop1  36502  neibastop2lem  36503  neibastop2  36504  rdgssun  37522  isbnd  37920  ismndo2  38014  rngomndo  38075  isidl  38154  ispsubsp  39944  sn-isghm  42858  isnacs  42888  mzpclval  42909  elmzpcl  42910  relpeq4  45130  permac8prim  45197  nelsubc3lem  49257  isthinc  49606