Theorem raleqbi1dv 3310

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∀wral 3052

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ral 3053  df-rex 3063

This theorem is referenced by:  raleqOLD  3312  isoeq4  7278  frrlem1  8240  frrlem13  8252  smo11  8308  dffi2  9340  inficl  9342  dffi3  9348  dfom3  9570  aceq1  10041  dfac5lem4  10050  dfac5lem4OLD  10052  kmlem1  10075  kmlem10  10084  kmlem13  10087  kmlem14  10088  cofsmo  10193  infpssrlem4  10230  axdc3lem2  10375  elwina  10611  elina  10612  iswun  10629  eltskg  10675  elgrug  10717  elnp  10912  elnpi  10913  dfnn2  12172  dfnn3  12173  dfuzi  12597  coprmprod  16602  coprmproddvds  16604  ismri  17568  isprs  18233  isdrs  18238  ispos  18251  pospropd  18262  istos  18353  isdlat  18459  isipodrs  18474  mgmhmpropd  18637  issubmgm  18641  mhmpropd  18731  issubm  18742  subgacs  19107  nsgacs  19108  isghm  19161  isghmOLD  19162  ghmeql  19185  iscmn  19735  isomnd  20069  rnghmval  20393  dfrhm2  20427  zrrnghm  20486  isorng  20811  islss  20902  lssacs  20935  lmhmeql  21024  islbs  21045  lbsextlem1  21130  lbsextlem3  21132  lbsextlem4  21133  isobs  21692  mat0dimcrng  22431  istopg  22856  isbasisg  22908  basis2  22912  eltg2  22919  iscldtop  23056  neipeltop  23090  isreg  23293  regsep  23295  isnrm  23296  islly  23429  isnlly  23430  llyi  23435  nllyi  23436  islly2  23445  cldllycmp  23456  isfbas  23790  fbssfi  23798  isust  24165  elutop  24194  ustuqtop  24207  utopsnneip  24209  ispsmet  24265  ismet  24284  isxmet  24285  metrest  24485  cncfval  24854  fmcfil  25245  iscfil3  25246  caucfil  25256  iscmet3  25266  cfilres  25269  minveclem3  25402  wilthlem2  27052  wilthlem3  27053  wilth  27054  dfn0s2  28345  dfconngr1  30281  isconngr  30282  1conngr  30287  isplig  30570  isgrpo  30591  isablo  30640  disjabrex  32675  disjabrexf  32676  isrnsiga  34297  isldsys  34340  isros  34352  issros  34359  bnj1286  35201  bnj1452  35234  kur14lem9  35436  cvmscbv  35480  cvmsi  35487  cvmsval  35488  neibastop1  36581  neibastop2lem  36582  neibastop2  36583  rdgssun  37660  isbnd  38060  ismndo2  38154  rngomndo  38215  isidl  38294  ispsubsp  40150  sn-isghm  43060  isnacs  43090  mzpclval  43111  elmzpcl  43112  relpeq4  45332  permac8prim  45399  nelsubc3lem  49458  isthinc  49807