Theorem raleqbi1dv 3335

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		raleqbi1dv.1	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))
3	1, 2	raleqbidvv 3333	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ral 3082  df-rex 3092

This theorem is used by:  isoeq4  7327  frrlem1  8289  frrlem13  8301  smo11  8357  dffi2  9390  inficl  9392  dffi3  9398  dfom3  9623  aceq1  10117  dfac5lem4  10126  kmlem1  10150  kmlem10  10159  kmlem13  10162  kmlem14  10163  cofsmo  10268  infpssrlem4  10305  axdc3lem2  10450  elwina  10690  elina  10691  iswun  10708  eltskg  10754  elgrug  10796  elnp  10991  elnpi  10992  dfnn2  12265  dfnn3  12266  dfuzi  12707  coprmprod  16745  coprmproddvds  16747  ismri  17713  isprs  18378  isdrs  18383  ispos  18396  pospropd  18407  istos  18498  isdlat  18604  isipodrs  18619  mgmhmpropd  18792  issubmgm  18796  mhmpropd  18891  issubm  18902  subgacs  19275  nsgacs  19276  isghm  19334  ghmeql  19357  iscmn  19907  isomnd  20241  rnghmval  20572  dfrhm2  20606  zrrnghm  20689  isorng  21018  islss  21109  lssacs  21142  lmhmeql  21230  islbs  21251  lbsextlem1  21336  lbsextlem3  21338  lbsextlem4  21339  isobs  21924  mat0dimcrng  22681  istopg  23106  isbasisg  23158  basis2  23162  eltg2  23169  iscldtop  23306  neipeltop  23340  isreg  23543  regsep  23545  isnrm  23546  islly  23680  isnlly  23681  llyi  23686  nllyi  23687  islly2  23696  cldllycmp  23707  isfbas  24041  fbssfi  24049  isust  24416  elutop  24445  ustuqtop  24458  utopsnneip  24460  ispsmet  24516  ismet  24535  isxmet  24536  metrest  24736  cncfval  25102  fmcfil  25486  iscfil3  25487  caucfil  25497  iscmet3  25507  cfilres  25510  minveclem3  25643  wilthlem2  27288  wilthlem3  27289  wilth  27290  dfn0s2  28580  dfconngr1  30614  isconngr  30615  1conngr  30620  isplig  30903  isgrpo  30924  isablo  30973  disjabrex  33002  disjabrexf  33003  isrnsiga  34571  isldsys  34615  isros  34627  issros  34634  bnj1286  35476  bnj1452  35509  kur14lem9  35747  cvmscbv  35791  cvmsi  35798  cvmsval  35799  nmulprop  36723  neibastop1  36931  neibastop2lem  36932  neibastop2  36933  dfttc4lem1  37100  rdgssun  38085  isbnd  38493  ismndo2  38587  rngomndo  38648  isidl  38727  ispsubsp  40581  sn-isghm  43482  isnacs  43512  mzpclval  43533  elmzpcl  43534  relpeq4  45733  permac8prim  45800  nelsubc3lem  49924  isthinc  50273