Theorem raleqbi1dv 3306

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 3304	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:  isoeq4  7270  frrlem1  8231  frrlem13  8243  smo11  8299  dffi2  9331  inficl  9333  dffi3  9339  dfom3  9563  aceq1  10034  dfac5lem4  10043  dfac5lem4OLD  10045  kmlem1  10068  kmlem10  10077  kmlem13  10080  kmlem14  10081  cofsmo  10186  infpssrlem4  10223  axdc3lem2  10368  elwina  10604  elina  10605  iswun  10622  eltskg  10668  elgrug  10710  elnp  10905  elnpi  10906  dfnn2  12182  dfnn3  12183  dfuzi  12615  coprmprod  16625  coprmproddvds  16627  ismri  17592  isprs  18257  isdrs  18262  ispos  18275  pospropd  18286  istos  18377  isdlat  18483  isipodrs  18498  mgmhmpropd  18661  issubmgm  18665  mhmpropd  18755  issubm  18766  subgacs  19131  nsgacs  19132  isghm  19185  isghmOLD  19186  ghmeql  19209  iscmn  19759  isomnd  20093  rnghmval  20415  dfrhm2  20449  zrrnghm  20508  isorng  20833  islss  20924  lssacs  20957  lmhmeql  21046  islbs  21067  lbsextlem1  21152  lbsextlem3  21154  lbsextlem4  21155  isobs  21714  mat0dimcrng  22449  istopg  22874  isbasisg  22926  basis2  22930  eltg2  22937  iscldtop  23074  neipeltop  23108  isreg  23311  regsep  23313  isnrm  23314  islly  23447  isnlly  23448  llyi  23453  nllyi  23454  islly2  23463  cldllycmp  23474  isfbas  23808  fbssfi  23816  isust  24183  elutop  24212  ustuqtop  24225  utopsnneip  24227  ispsmet  24283  ismet  24302  isxmet  24303  metrest  24503  cncfval  24869  fmcfil  25253  iscfil3  25254  caucfil  25264  iscmet3  25274  cfilres  25277  minveclem3  25410  wilthlem2  27050  wilthlem3  27051  wilth  27052  dfn0s2  28342  dfconngr1  30277  isconngr  30278  1conngr  30283  isplig  30566  isgrpo  30587  isablo  30636  disjabrex  32671  disjabrexf  32672  isrnsiga  34277  isldsys  34320  isros  34332  issros  34339  bnj1286  35181  bnj1452  35214  kur14lem9  35416  cvmscbv  35460  cvmsi  35467  cvmsval  35468  neibastop1  36561  neibastop2lem  36562  neibastop2  36563  dfttc4lem1  36730  rdgssun  37712  isbnd  38119  ismndo2  38213  rngomndo  38274  isidl  38353  ispsubsp  40209  sn-isghm  43124  isnacs  43154  mzpclval  43175  elmzpcl  43176  relpeq4  45396  permac8prim  45463  nelsubc3lem  49561  isthinc  49910