Theorem raleqbi1dv 3332

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1562  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-ral 3079  df-rex 3089

This theorem is referenced by:  isoeq4  7306  frrlem1  8269  frrlem13  8281  smo11  8337  dffi2  9371  inficl  9373  dffi3  9379  dfom3  9604  aceq1  10075  dfac5lem4  10084  dfac5lem4OLD  10086  kmlem1  10109  kmlem10  10118  kmlem13  10121  kmlem14  10122  cofsmo  10228  infpssrlem4  10265  axdc3lem2  10410  elwina  10646  elina  10647  iswun  10664  eltskg  10710  elgrug  10752  elnp  10947  elnpi  10948  dfnn2  12225  dfnn3  12226  dfuzi  12666  coprmprod  16697  coprmproddvds  16699  ismri  17665  isprs  18330  isdrs  18335  ispos  18348  pospropd  18359  istos  18450  isdlat  18556  isipodrs  18571  mgmhmpropd  18734  issubmgm  18738  mhmpropd  18828  issubm  18839  subgacs  19204  nsgacs  19205  isghm  19258  ghmeql  19281  iscmn  19831  isomnd  20165  rnghmval  20491  dfrhm2  20525  zrrnghm  20588  isorng  20912  islss  21003  lssacs  21036  lmhmeql  21124  islbs  21145  lbsextlem1  21230  lbsextlem3  21232  lbsextlem4  21233  isobs  21774  mat0dimcrng  22532  istopg  22957  isbasisg  23009  basis2  23013  eltg2  23020  iscldtop  23157  neipeltop  23191  isreg  23394  regsep  23396  isnrm  23397  islly  23530  isnlly  23531  llyi  23536  nllyi  23537  islly2  23546  cldllycmp  23557  isfbas  23891  fbssfi  23899  isust  24266  elutop  24295  ustuqtop  24308  utopsnneip  24310  ispsmet  24366  ismet  24385  isxmet  24386  metrest  24586  cncfval  24952  fmcfil  25336  iscfil3  25337  caucfil  25347  iscmet3  25357  cfilres  25360  minveclem3  25493  wilthlem2  27135  wilthlem3  27136  wilth  27137  dfn0s2  28427  dfconngr1  30392  isconngr  30393  1conngr  30398  isplig  30681  isgrpo  30702  isablo  30751  disjabrex  32784  disjabrexf  32785  isrnsiga  34412  isldsys  34455  isros  34467  issros  34474  bnj1286  35316  bnj1452  35349  kur14lem9  35569  cvmscbv  35613  cvmsi  35620  cvmsval  35621  nmulprop  36545  neibastop1  36724  neibastop2lem  36725  neibastop2  36726  dfttc4lem1  36893  rdgssun  37877  isbnd  38284  ismndo2  38378  rngomndo  38439  isidl  38518  ispsubsp  40374  sn-isghm  43260  isnacs  43290  mzpclval  43311  elmzpcl  43312  relpeq4  45528  permac8prim  45595  nelsubc3lem  49696  isthinc  50045