Theorem raleqbi1dv 3334

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ral 3063  df-rex 3072

This theorem is referenced by:  raleqOLD  3336  isoeq4  7317  frrlem1  8271  frrlem13  8283  wfrlem1OLD  8308  wfrlem4OLD  8312  wfrlem15OLD  8323  smo11  8364  dffi2  9418  inficl  9420  dffi3  9426  dfom3  9642  aceq1  10112  dfac5lem4  10121  kmlem1  10145  kmlem10  10154  kmlem13  10157  kmlem14  10158  cofsmo  10264  infpssrlem4  10301  axdc3lem2  10446  elwina  10681  elina  10682  iswun  10699  eltskg  10745  elgrug  10787  elnp  10982  elnpi  10983  dfnn2  12225  dfnn3  12226  dfuzi  12653  coprmprod  16598  coprmproddvds  16600  ismri  17575  isprs  18250  isdrs  18254  ispos  18267  pospropd  18280  istos  18371  isdlat  18475  isipodrs  18490  mhmpropd  18678  issubm  18684  subgacs  19041  nsgacs  19042  isghm  19092  ghmeql  19115  iscmn  19657  dfrhm2  20253  islss  20545  lssacs  20578  lmhmeql  20666  islbs  20687  lbsextlem1  20771  lbsextlem3  20773  lbsextlem4  20774  isobs  21275  mat0dimcrng  21972  istopg  22397  isbasisg  22450  basis2  22454  eltg2  22461  iscldtop  22599  neipeltop  22633  isreg  22836  regsep  22838  isnrm  22839  islly  22972  isnlly  22973  llyi  22978  nllyi  22979  islly2  22988  cldllycmp  22999  isfbas  23333  fbssfi  23341  isust  23708  elutop  23738  ustuqtop  23751  utopsnneip  23753  ispsmet  23810  ismet  23829  isxmet  23830  metrest  24033  cncfval  24404  fmcfil  24789  iscfil3  24790  caucfil  24800  iscmet3  24810  cfilres  24813  minveclem3  24946  wilthlem2  26573  wilthlem3  26574  wilth  26575  dfconngr1  29441  isconngr  29442  1conngr  29447  isplig  29729  isgrpo  29750  isablo  29799  disjabrex  31813  disjabrexf  31814  isomnd  32219  isorng  32417  isrnsiga  33111  isldsys  33154  isros  33166  issros  33173  bnj1286  34030  bnj1452  34063  kur14lem9  34205  cvmscbv  34249  cvmsi  34256  cvmsval  34257  neibastop1  35244  neibastop2lem  35245  neibastop2  35246  rdgssun  36259  isbnd  36648  ismndo2  36742  rngomndo  36803  isidl  36882  ispsubsp  38616  isnacs  41442  mzpclval  41463  elmzpcl  41464  mgmhmpropd  46555  issubmgm  46559  rnghmval  46689  zrrnghm  46716  isthinc  47641