Theorem raleqbi1dv 3331

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∀wral 3059

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-ral 3060  df-rex 3069

This theorem is referenced by:  raleqOLD  3333  isoeq4  7319  frrlem1  8273  frrlem13  8285  wfrlem1OLD  8310  wfrlem4OLD  8314  wfrlem15OLD  8325  smo11  8366  dffi2  9420  inficl  9422  dffi3  9428  dfom3  9644  aceq1  10114  dfac5lem4  10123  kmlem1  10147  kmlem10  10156  kmlem13  10159  kmlem14  10160  cofsmo  10266  infpssrlem4  10303  axdc3lem2  10448  elwina  10683  elina  10684  iswun  10701  eltskg  10747  elgrug  10789  elnp  10984  elnpi  10985  dfnn2  12229  dfnn3  12230  dfuzi  12657  coprmprod  16602  coprmproddvds  16604  ismri  17579  isprs  18254  isdrs  18258  ispos  18271  pospropd  18284  istos  18375  isdlat  18479  isipodrs  18494  mgmhmpropd  18623  issubmgm  18627  mhmpropd  18714  issubm  18720  subgacs  19077  nsgacs  19078  isghm  19130  ghmeql  19153  iscmn  19698  rnghmval  20331  dfrhm2  20365  zrrnghm  20425  islss  20689  lssacs  20722  lmhmeql  20810  islbs  20831  lbsextlem1  20916  lbsextlem3  20918  lbsextlem4  20919  isobs  21494  mat0dimcrng  22192  istopg  22617  isbasisg  22670  basis2  22674  eltg2  22681  iscldtop  22819  neipeltop  22853  isreg  23056  regsep  23058  isnrm  23059  islly  23192  isnlly  23193  llyi  23198  nllyi  23199  islly2  23208  cldllycmp  23219  isfbas  23553  fbssfi  23561  isust  23928  elutop  23958  ustuqtop  23971  utopsnneip  23973  ispsmet  24030  ismet  24049  isxmet  24050  metrest  24253  cncfval  24628  fmcfil  25020  iscfil3  25021  caucfil  25031  iscmet3  25041  cfilres  25044  minveclem3  25177  wilthlem2  26809  wilthlem3  26810  wilth  26811  dfn0s2  27941  dfconngr1  29708  isconngr  29709  1conngr  29714  isplig  29996  isgrpo  30017  isablo  30066  disjabrex  32080  disjabrexf  32081  isomnd  32489  isorng  32687  isrnsiga  33409  isldsys  33452  isros  33464  issros  33471  bnj1286  34328  bnj1452  34361  kur14lem9  34503  cvmscbv  34547  cvmsi  34554  cvmsval  34555  neibastop1  35547  neibastop2lem  35548  neibastop2  35549  rdgssun  36562  isbnd  36951  ismndo2  37045  rngomndo  37106  isidl  37185  ispsubsp  38919  isnacs  41744  mzpclval  41765  elmzpcl  41766  isthinc  47728