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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-cleq 2729  df-ral 3063

This theorem is referenced by:  raleq  3306  isoeq4  7251  frrlem1  8176  frrlem13  8188  wfrlem1OLD  8213  wfrlem4OLD  8217  wfrlem15OLD  8228  smo11  8269  dffi2  9284  inficl  9286  dffi3  9292  dfom3  9508  aceq1  9978  dfac5lem4  9987  kmlem1  10011  kmlem10  10020  kmlem13  10023  kmlem14  10024  cofsmo  10130  infpssrlem4  10167  axdc3lem2  10312  elwina  10547  elina  10548  iswun  10565  eltskg  10611  elgrug  10653  elnp  10848  elnpi  10849  dfnn2  12091  dfnn3  12092  dfuzi  12516  coprmprod  16463  coprmproddvds  16465  ismri  17437  isprs  18112  isdrs  18116  ispos  18129  pospropd  18142  istos  18233  isdlat  18337  isipodrs  18352  mhmpropd  18533  issubm  18539  subgacs  18885  nsgacs  18886  isghm  18930  ghmeql  18953  iscmn  19489  dfrhm2  20055  islss  20301  lssacs  20334  lmhmeql  20422  islbs  20443  lbsextlem1  20525  lbsextlem3  20527  lbsextlem4  20528  isobs  21032  mat0dimcrng  21724  istopg  22149  isbasisg  22202  basis2  22206  eltg2  22213  iscldtop  22351  neipeltop  22385  isreg  22588  regsep  22590  isnrm  22591  islly  22724  isnlly  22725  llyi  22730  nllyi  22731  islly2  22740  cldllycmp  22751  isfbas  23085  fbssfi  23093  isust  23460  elutop  23490  ustuqtop  23503  utopsnneip  23505  ispsmet  23562  ismet  23581  isxmet  23582  metrest  23785  cncfval  24156  fmcfil  24541  iscfil3  24542  caucfil  24552  iscmet3  24562  cfilres  24565  minveclem3  24698  wilthlem2  26323  wilthlem3  26324  wilth  26325  dfconngr1  28839  isconngr  28840  1conngr  28845  isplig  29125  isgrpo  29146  isablo  29195  disjabrex  31206  disjabrexf  31207  isomnd  31612  isorng  31796  isrnsiga  32377  isldsys  32420  isros  32432  issros  32439  bnj1286  33296  bnj1452  33329  kur14lem9  33473  cvmscbv  33517  cvmsi  33524  cvmsval  33525  neibastop1  34685  neibastop2lem  34686  neibastop2  34687  rdgssun  35703  isbnd  36094  ismndo2  36188  rngomndo  36249  isidl  36328  ispsubsp  38064  isnacs  40839  mzpclval  40860  elmzpcl  40861  mgmhmpropd  45757  issubmgm  45761  rnghmval  45867  zrrnghm  45893  isthinc  46720