Theorem raleqbi1dv 3341

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∀wral 3065

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-ral 3070

This theorem is referenced by:  raleq  3343  isoeq4  7200  frrlem1  8111  frrlem13  8123  wfrlem1OLD  8148  wfrlem4OLD  8152  wfrlem15OLD  8163  smo11  8204  dffi2  9191  inficl  9193  dffi3  9199  dfom3  9414  aceq1  9882  dfac5lem4  9891  kmlem1  9915  kmlem10  9924  kmlem13  9927  kmlem14  9928  cofsmo  10034  infpssrlem4  10071  axdc3lem2  10216  elwina  10451  elina  10452  iswun  10469  eltskg  10515  elgrug  10557  elnp  10752  elnpi  10753  dfnn2  11995  dfnn3  11996  dfuzi  12420  coprmprod  16375  coprmproddvds  16377  ismri  17349  isprs  18024  isdrs  18028  ispos  18041  pospropd  18054  istos  18145  isdlat  18249  isipodrs  18264  mhmpropd  18445  issubm  18451  subgacs  18798  nsgacs  18799  isghm  18843  ghmeql  18866  iscmn  19403  dfrhm2  19970  islss  20205  lssacs  20238  lmhmeql  20326  islbs  20347  lbsextlem1  20429  lbsextlem3  20431  lbsextlem4  20432  isobs  20936  mat0dimcrng  21628  istopg  22053  isbasisg  22106  basis2  22110  eltg2  22117  iscldtop  22255  neipeltop  22289  isreg  22492  regsep  22494  isnrm  22495  islly  22628  isnlly  22629  llyi  22634  nllyi  22635  islly2  22644  cldllycmp  22655  isfbas  22989  fbssfi  22997  isust  23364  elutop  23394  ustuqtop  23407  utopsnneip  23409  ispsmet  23466  ismet  23485  isxmet  23486  metrest  23689  cncfval  24060  fmcfil  24445  iscfil3  24446  caucfil  24456  iscmet3  24466  cfilres  24469  minveclem3  24602  wilthlem2  26227  wilthlem3  26228  wilth  26229  dfconngr1  28561  isconngr  28562  1conngr  28567  isplig  28847  isgrpo  28868  isablo  28917  disjabrex  30930  disjabrexf  30931  isomnd  31336  isorng  31507  isrnsiga  32090  isldsys  32133  isros  32145  issros  32152  bnj1286  33008  bnj1452  33041  kur14lem9  33185  cvmscbv  33229  cvmsi  33236  cvmsval  33237  neibastop1  34557  neibastop2lem  34558  neibastop2  34559  rdgssun  35558  isbnd  35947  ismndo2  36041  rngomndo  36102  isidl  36181  ispsubsp  37766  isnacs  40533  mzpclval  40554  elmzpcl  40555  mgmhmpropd  45350  issubmgm  45354  rnghmval  45460  zrrnghm  45486  isthinc  46313