Theorem raleqbi1dv 3323

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  ∀wral 3051

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ral 3052  df-rex 3061

This theorem is referenced by:  raleqOLD  3325  isoeq4  7332  frrlem1  8301  frrlem13  8313  wfrlem1OLD  8338  wfrlem4OLD  8342  wfrlem15OLD  8353  smo11  8394  dffi2  9466  inficl  9468  dffi3  9474  dfom3  9690  aceq1  10160  dfac5lem4  10169  kmlem1  10193  kmlem10  10202  kmlem13  10205  kmlem14  10206  cofsmo  10312  infpssrlem4  10349  axdc3lem2  10494  elwina  10729  elina  10730  iswun  10747  eltskg  10793  elgrug  10835  elnp  11030  elnpi  11031  dfnn2  12277  dfnn3  12278  dfuzi  12705  coprmprod  16662  coprmproddvds  16664  ismri  17644  isprs  18322  isdrs  18326  ispos  18339  pospropd  18352  istos  18443  isdlat  18547  isipodrs  18562  mgmhmpropd  18691  issubmgm  18695  mhmpropd  18782  issubm  18793  subgacs  19155  nsgacs  19156  isghm  19209  isghmOLD  19210  ghmeql  19233  iscmn  19787  rnghmval  20422  dfrhm2  20456  zrrnghm  20518  islss  20911  lssacs  20944  lmhmeql  21033  islbs  21054  lbsextlem1  21139  lbsextlem3  21141  lbsextlem4  21142  isobs  21718  mat0dimcrng  22463  istopg  22888  isbasisg  22941  basis2  22945  eltg2  22952  iscldtop  23090  neipeltop  23124  isreg  23327  regsep  23329  isnrm  23330  islly  23463  isnlly  23464  llyi  23469  nllyi  23470  islly2  23479  cldllycmp  23490  isfbas  23824  fbssfi  23832  isust  24199  elutop  24229  ustuqtop  24242  utopsnneip  24244  ispsmet  24301  ismet  24320  isxmet  24321  metrest  24524  cncfval  24899  fmcfil  25291  iscfil3  25292  caucfil  25302  iscmet3  25312  cfilres  25315  minveclem3  25448  wilthlem2  27097  wilthlem3  27098  wilth  27099  dfn0s2  28304  dfconngr1  30121  isconngr  30122  1conngr  30127  isplig  30409  isgrpo  30430  isablo  30479  disjabrex  32502  disjabrexf  32503  isomnd  32936  isorng  33177  isrnsiga  33946  isldsys  33989  isros  34001  issros  34008  bnj1286  34864  bnj1452  34897  kur14lem9  35042  cvmscbv  35086  cvmsi  35093  cvmsval  35094  neibastop1  36071  neibastop2lem  36072  neibastop2  36073  rdgssun  37085  isbnd  37481  ismndo2  37575  rngomndo  37636  isidl  37715  ispsubsp  39444  sn-isghm  42327  isnacs  42361  mzpclval  42382  elmzpcl  42383  isthinc  48342