Theorem raleqbi1dv 3301

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 3297	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  3303  isoeq4  7257  frrlem1  8219  frrlem13  8231  smo11  8287  dffi2  9313  inficl  9315  dffi3  9321  dfom3  9543  aceq1  10011  dfac5lem4  10020  dfac5lem4OLD  10022  kmlem1  10045  kmlem10  10054  kmlem13  10057  kmlem14  10058  cofsmo  10163  infpssrlem4  10200  axdc3lem2  10345  elwina  10580  elina  10581  iswun  10598  eltskg  10644  elgrug  10686  elnp  10881  elnpi  10882  dfnn2  12141  dfnn3  12142  dfuzi  12567  coprmprod  16572  coprmproddvds  16574  ismri  17537  isprs  18202  isdrs  18207  ispos  18220  pospropd  18231  istos  18322  isdlat  18428  isipodrs  18443  mgmhmpropd  18572  issubmgm  18576  mhmpropd  18666  issubm  18677  subgacs  19040  nsgacs  19041  isghm  19094  isghmOLD  19095  ghmeql  19118  iscmn  19668  isomnd  20002  rnghmval  20325  dfrhm2  20359  zrrnghm  20421  isorng  20746  islss  20837  lssacs  20870  lmhmeql  20959  islbs  20980  lbsextlem1  21065  lbsextlem3  21067  lbsextlem4  21068  isobs  21627  mat0dimcrng  22355  istopg  22780  isbasisg  22832  basis2  22836  eltg2  22843  iscldtop  22980  neipeltop  23014  isreg  23217  regsep  23219  isnrm  23220  islly  23353  isnlly  23354  llyi  23359  nllyi  23360  islly2  23369  cldllycmp  23380  isfbas  23714  fbssfi  23722  isust  24089  elutop  24119  ustuqtop  24132  utopsnneip  24134  ispsmet  24190  ismet  24209  isxmet  24210  metrest  24410  cncfval  24779  fmcfil  25170  iscfil3  25171  caucfil  25181  iscmet3  25191  cfilres  25194  minveclem3  25327  wilthlem2  26977  wilthlem3  26978  wilth  26979  dfn0s2  28229  dfconngr1  30132  isconngr  30133  1conngr  30138  isplig  30420  isgrpo  30441  isablo  30490  disjabrex  32526  disjabrexf  32527  isrnsiga  34086  isldsys  34129  isros  34141  issros  34148  bnj1286  34992  bnj1452  35025  kur14lem9  35197  cvmscbv  35241  cvmsi  35248  cvmsval  35249  neibastop1  36343  neibastop2lem  36344  neibastop2  36345  rdgssun  37362  isbnd  37770  ismndo2  37864  rngomndo  37925  isidl  38004  ispsubsp  39734  sn-isghm  42656  isnacs  42687  mzpclval  42708  elmzpcl  42709  relpeq4  44931  permac8prim  44998  nelsubc3lem  49065  isthinc  49414