Theorem raleqbi1dv 3331

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ral 3068

This theorem is referenced by:  raleq  3333  isoeq4  7171  frrlem1  8073  frrlem13  8085  wfrlem1OLD  8110  wfrlem4OLD  8114  wfrlem15OLD  8125  smo11  8166  dffi2  9112  inficl  9114  dffi3  9120  dfom3  9335  aceq1  9804  dfac5lem4  9813  kmlem1  9837  kmlem10  9846  kmlem13  9849  kmlem14  9850  cofsmo  9956  infpssrlem4  9993  axdc3lem2  10138  elwina  10373  elina  10374  iswun  10391  eltskg  10437  elgrug  10479  elnp  10674  elnpi  10675  dfnn2  11916  dfnn3  11917  dfuzi  12341  coprmprod  16294  coprmproddvds  16296  ismri  17257  isprs  17930  isdrs  17934  ispos  17947  pospropd  17960  istos  18051  isdlat  18155  isipodrs  18170  mhmpropd  18351  issubm  18357  subgacs  18704  nsgacs  18705  isghm  18749  ghmeql  18772  iscmn  19309  dfrhm2  19876  islss  20111  lssacs  20144  lmhmeql  20232  islbs  20253  lbsextlem1  20335  lbsextlem3  20337  lbsextlem4  20338  isobs  20837  mat0dimcrng  21527  istopg  21952  isbasisg  22005  basis2  22009  eltg2  22016  iscldtop  22154  neipeltop  22188  isreg  22391  regsep  22393  isnrm  22394  islly  22527  isnlly  22528  llyi  22533  nllyi  22534  islly2  22543  cldllycmp  22554  isfbas  22888  fbssfi  22896  isust  23263  elutop  23293  ustuqtop  23306  utopsnneip  23308  ispsmet  23365  ismet  23384  isxmet  23385  metrest  23586  cncfval  23957  fmcfil  24341  iscfil3  24342  caucfil  24352  iscmet3  24362  cfilres  24365  minveclem3  24498  wilthlem2  26123  wilthlem3  26124  wilth  26125  dfconngr1  28453  isconngr  28454  1conngr  28459  isplig  28739  isgrpo  28760  isablo  28809  disjabrex  30822  disjabrexf  30823  isomnd  31229  isorng  31400  isrnsiga  31981  isldsys  32024  isros  32036  issros  32043  bnj1286  32899  bnj1452  32932  kur14lem9  33076  cvmscbv  33120  cvmsi  33127  cvmsval  33128  neibastop1  34475  neibastop2lem  34476  neibastop2  34477  rdgssun  35476  isbnd  35865  ismndo2  35959  rngomndo  36020  isidl  36099  ispsubsp  37686  isnacs  40442  mzpclval  40463  elmzpcl  40464  mgmhmpropd  45227  issubmgm  45231  rnghmval  45337  zrrnghm  45363  isthinc  46190