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

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

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 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ral 3050  df-rex 3059

This theorem is referenced by:  raleqOLD  3308  isoeq4  7263  frrlem1  8225  frrlem13  8237  smo11  8293  dffi2  9317  inficl  9319  dffi3  9325  dfom3  9547  aceq1  10018  dfac5lem4  10027  dfac5lem4OLD  10029  kmlem1  10052  kmlem10  10061  kmlem13  10064  kmlem14  10065  cofsmo  10170  infpssrlem4  10207  axdc3lem2  10352  elwina  10587  elina  10588  iswun  10605  eltskg  10651  elgrug  10693  elnp  10888  elnpi  10889  dfnn2  12148  dfnn3  12149  dfuzi  12574  coprmprod  16582  coprmproddvds  16584  ismri  17547  isprs  18212  isdrs  18217  ispos  18230  pospropd  18241  istos  18332  isdlat  18438  isipodrs  18453  mgmhmpropd  18616  issubmgm  18620  mhmpropd  18710  issubm  18721  subgacs  19083  nsgacs  19084  isghm  19137  isghmOLD  19138  ghmeql  19161  iscmn  19711  isomnd  20045  rnghmval  20368  dfrhm2  20402  zrrnghm  20461  isorng  20786  islss  20877  lssacs  20910  lmhmeql  20999  islbs  21020  lbsextlem1  21105  lbsextlem3  21107  lbsextlem4  21108  isobs  21667  mat0dimcrng  22395  istopg  22820  isbasisg  22872  basis2  22876  eltg2  22883  iscldtop  23020  neipeltop  23054  isreg  23257  regsep  23259  isnrm  23260  islly  23393  isnlly  23394  llyi  23399  nllyi  23400  islly2  23409  cldllycmp  23420  isfbas  23754  fbssfi  23762  isust  24129  elutop  24158  ustuqtop  24171  utopsnneip  24173  ispsmet  24229  ismet  24248  isxmet  24249  metrest  24449  cncfval  24818  fmcfil  25209  iscfil3  25210  caucfil  25220  iscmet3  25230  cfilres  25233  minveclem3  25366  wilthlem2  27016  wilthlem3  27017  wilth  27018  dfn0s2  28270  dfconngr1  30179  isconngr  30180  1conngr  30185  isplig  30467  isgrpo  30488  isablo  30537  disjabrex  32573  disjabrexf  32574  isrnsiga  34137  isldsys  34180  isros  34192  issros  34199  bnj1286  35042  bnj1452  35075  kur14lem9  35269  cvmscbv  35313  cvmsi  35320  cvmsval  35321  neibastop1  36414  neibastop2lem  36415  neibastop2  36416  rdgssun  37433  isbnd  37830  ismndo2  37924  rngomndo  37985  isidl  38064  ispsubsp  39854  sn-isghm  42781  isnacs  42811  mzpclval  42832  elmzpcl  42833  relpeq4  45054  permac8prim  45121  nelsubc3lem  49185  isthinc  49534