Theorem raleqbi1dv 3311

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ral 3045  df-rex 3054

This theorem is referenced by:  raleqOLD  3313  isoeq4  7295  frrlem1  8265  frrlem13  8277  smo11  8333  dffi2  9374  inficl  9376  dffi3  9382  dfom3  9600  aceq1  10070  dfac5lem4  10079  dfac5lem4OLD  10081  kmlem1  10104  kmlem10  10113  kmlem13  10116  kmlem14  10117  cofsmo  10222  infpssrlem4  10259  axdc3lem2  10404  elwina  10639  elina  10640  iswun  10657  eltskg  10703  elgrug  10745  elnp  10940  elnpi  10941  dfnn2  12199  dfnn3  12200  dfuzi  12625  coprmprod  16631  coprmproddvds  16633  ismri  17592  isprs  18257  isdrs  18262  ispos  18275  pospropd  18286  istos  18377  isdlat  18481  isipodrs  18496  mgmhmpropd  18625  issubmgm  18629  mhmpropd  18719  issubm  18730  subgacs  19093  nsgacs  19094  isghm  19147  isghmOLD  19148  ghmeql  19171  iscmn  19719  rnghmval  20349  dfrhm2  20383  zrrnghm  20445  islss  20840  lssacs  20873  lmhmeql  20962  islbs  20983  lbsextlem1  21068  lbsextlem3  21070  lbsextlem4  21071  isobs  21629  mat0dimcrng  22357  istopg  22782  isbasisg  22834  basis2  22838  eltg2  22845  iscldtop  22982  neipeltop  23016  isreg  23219  regsep  23221  isnrm  23222  islly  23355  isnlly  23356  llyi  23361  nllyi  23362  islly2  23371  cldllycmp  23382  isfbas  23716  fbssfi  23724  isust  24091  elutop  24121  ustuqtop  24134  utopsnneip  24136  ispsmet  24192  ismet  24211  isxmet  24212  metrest  24412  cncfval  24781  fmcfil  25172  iscfil3  25173  caucfil  25183  iscmet3  25193  cfilres  25196  minveclem3  25329  wilthlem2  26979  wilthlem3  26980  wilth  26981  dfn0s2  28224  dfconngr1  30117  isconngr  30118  1conngr  30123  isplig  30405  isgrpo  30426  isablo  30475  disjabrex  32511  disjabrexf  32512  isomnd  33015  isorng  33277  isrnsiga  34103  isldsys  34146  isros  34158  issros  34165  bnj1286  35009  bnj1452  35042  kur14lem9  35201  cvmscbv  35245  cvmsi  35252  cvmsval  35253  neibastop1  36347  neibastop2lem  36348  neibastop2  36349  rdgssun  37366  isbnd  37774  ismndo2  37868  rngomndo  37929  isidl  38008  ispsubsp  39739  sn-isghm  42661  isnacs  42692  mzpclval  42713  elmzpcl  42714  relpeq4  44937  permac8prim  45004  nelsubc3lem  49059  isthinc  49408