Theorem raleqbi1dv 3310

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  ∀wral 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2706

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2726  df-ral 3059

This theorem is referenced by:  raleq  3312  isoeq4  7118  frrlem1  8016  frrlem13  8028  wfrlem1  8043  wfrlem4  8047  wfrlem15  8058  smo11  8090  dffi2  9028  inficl  9030  dffi3  9036  dfom3  9251  aceq1  9714  dfac5lem4  9723  kmlem1  9747  kmlem10  9756  kmlem13  9759  kmlem14  9760  cofsmo  9866  infpssrlem4  9903  axdc3lem2  10048  elwina  10283  elina  10284  iswun  10301  eltskg  10347  elgrug  10389  elnp  10584  elnpi  10585  dfnn2  11826  dfnn3  11827  dfuzi  12251  coprmprod  16199  coprmproddvds  16201  ismri  17106  isprs  17776  isdrs  17780  ispos  17793  pospropd  17805  istos  17896  isdlat  18000  isipodrs  18015  mhmpropd  18196  issubm  18202  subgacs  18549  nsgacs  18550  isghm  18594  ghmeql  18617  iscmn  19150  dfrhm2  19709  islss  19943  lssacs  19976  lmhmeql  20064  islbs  20085  lbsextlem1  20167  lbsextlem3  20169  lbsextlem4  20170  isobs  20654  mat0dimcrng  21339  istopg  21764  isbasisg  21816  basis2  21820  eltg2  21827  iscldtop  21964  neipeltop  21998  isreg  22201  regsep  22203  isnrm  22204  islly  22337  isnlly  22338  llyi  22343  nllyi  22344  islly2  22353  cldllycmp  22364  isfbas  22698  fbssfi  22706  isust  23073  elutop  23103  ustuqtop  23116  utopsnneip  23118  ispsmet  23174  ismet  23193  isxmet  23194  metrest  23394  cncfval  23757  fmcfil  24141  iscfil3  24142  caucfil  24152  iscmet3  24162  cfilres  24165  minveclem3  24298  wilthlem2  25923  wilthlem3  25924  wilth  25925  dfconngr1  28243  isconngr  28244  1conngr  28249  isplig  28529  isgrpo  28550  isablo  28599  disjabrex  30612  disjabrexf  30613  isomnd  31018  isorng  31189  isrnsiga  31765  isldsys  31808  isros  31820  issros  31827  bnj1286  32684  bnj1452  32717  kur14lem9  32861  cvmscbv  32905  cvmsi  32912  cvmsval  32913  neibastop1  34242  neibastop2lem  34243  neibastop2  34244  rdgssun  35243  isbnd  35632  ismndo2  35726  rngomndo  35787  isidl  35866  ispsubsp  37453  isnacs  40181  mzpclval  40202  elmzpcl  40203  mgmhmpropd  44966  issubmgm  44970  rnghmval  45076  zrrnghm  45102  isthinc  45929