Theorem raleqbi1dv 3304

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ral 3048  df-rex 3057

This theorem is referenced by:  raleqOLD  3306  isoeq4  7254  frrlem1  8216  frrlem13  8228  smo11  8284  dffi2  9307  inficl  9309  dffi3  9315  dfom3  9537  aceq1  10008  dfac5lem4  10017  dfac5lem4OLD  10019  kmlem1  10042  kmlem10  10051  kmlem13  10054  kmlem14  10055  cofsmo  10160  infpssrlem4  10197  axdc3lem2  10342  elwina  10577  elina  10578  iswun  10595  eltskg  10641  elgrug  10683  elnp  10878  elnpi  10879  dfnn2  12138  dfnn3  12139  dfuzi  12564  coprmprod  16572  coprmproddvds  16574  ismri  17537  isprs  18202  isdrs  18207  ispos  18220  pospropd  18231  istos  18322  isdlat  18428  isipodrs  18443  mgmhmpropd  18606  issubmgm  18610  mhmpropd  18700  issubm  18711  subgacs  19073  nsgacs  19074  isghm  19127  isghmOLD  19128  ghmeql  19151  iscmn  19701  isomnd  20035  rnghmval  20358  dfrhm2  20392  zrrnghm  20451  isorng  20776  islss  20867  lssacs  20900  lmhmeql  20989  islbs  21010  lbsextlem1  21095  lbsextlem3  21097  lbsextlem4  21098  isobs  21657  mat0dimcrng  22385  istopg  22810  isbasisg  22862  basis2  22866  eltg2  22873  iscldtop  23010  neipeltop  23044  isreg  23247  regsep  23249  isnrm  23250  islly  23383  isnlly  23384  llyi  23389  nllyi  23390  islly2  23399  cldllycmp  23410  isfbas  23744  fbssfi  23752  isust  24119  elutop  24148  ustuqtop  24161  utopsnneip  24163  ispsmet  24219  ismet  24238  isxmet  24239  metrest  24439  cncfval  24808  fmcfil  25199  iscfil3  25200  caucfil  25210  iscmet3  25220  cfilres  25223  minveclem3  25356  wilthlem2  27006  wilthlem3  27007  wilth  27008  dfn0s2  28260  dfconngr1  30168  isconngr  30169  1conngr  30174  isplig  30456  isgrpo  30477  isablo  30526  disjabrex  32562  disjabrexf  32563  isrnsiga  34126  isldsys  34169  isros  34181  issros  34188  bnj1286  35031  bnj1452  35064  kur14lem9  35258  cvmscbv  35302  cvmsi  35309  cvmsval  35310  neibastop1  36403  neibastop2lem  36404  neibastop2  36405  rdgssun  37422  isbnd  37830  ismndo2  37924  rngomndo  37985  isidl  38064  ispsubsp  39854  sn-isghm  42776  isnacs  42807  mzpclval  42828  elmzpcl  42829  relpeq4  45050  permac8prim  45117  nelsubc3lem  49181  isthinc  49530