Theorem raleqbi1dv 3337

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1507  ∀wral 3082

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-clel 2840  df-ral 3087

This theorem is referenced by:  raleq  3339  isoeq4  6890  wfrlem1  7750  wfrlem4  7754  wfrlem4OLD  7755  wfrlem15  7766  smo11  7798  dffi2  8674  inficl  8676  dffi3  8682  dfom3  8896  aceq1  9329  dfac5lem4  9338  kmlem1  9362  kmlem10  9371  kmlem13  9374  kmlem14  9375  cofsmo  9481  infpssrlem4  9518  axdc3lem2  9663  elwina  9898  elina  9899  iswun  9916  eltskg  9962  elgrug  10004  elnp  10199  elnpi  10200  dfnn2  11446  dfnn3  11447  dfuzi  11879  coprmprod  15851  coprmproddvds  15853  ismri  16750  isprs  17388  isdrs  17392  ispos  17405  istos  17493  pospropd  17592  isipodrs  17619  isdlat  17651  mhmpropd  17799  issubm  17805  subgacs  18088  nsgacs  18089  isghm  18119  ghmeql  18142  iscmn  18663  dfrhm2  19182  islss  19418  lssacs  19451  lmhmeql  19539  islbs  19560  lbsextlem1  19642  lbsextlem3  19644  lbsextlem4  19645  isobs  20556  mat0dimcrng  20773  istopg  21197  isbasisg  21249  basis2  21253  eltg2  21260  iscldtop  21397  neipeltop  21431  isreg  21634  regsep  21636  isnrm  21637  islly  21770  isnlly  21771  llyi  21776  nllyi  21777  islly2  21786  cldllycmp  21797  isfbas  22131  fbssfi  22139  isust  22505  elutop  22535  ustuqtop  22548  utopsnneip  22550  ispsmet  22607  ismet  22626  isxmet  22627  metrest  22827  cncfval  23189  fmcfil  23568  iscfil3  23569  caucfil  23579  iscmet3  23589  cfilres  23592  minveclem3  23725  wilthlem2  25338  wilthlem3  25339  wilth  25340  dfconngr1  27707  isconngr  27708  1conngr  27713  isplig  28020  isgrpo  28041  isablo  28090  disjabrex  30088  disjabrexf  30089  isomnd  30398  isorng  30507  isrnsigaOLD  30973  isrnsiga  30974  isldsys  31017  isros  31029  issros  31036  bnj1286  31897  bnj1452  31930  kur14lem9  32006  cvmscbv  32050  cvmsi  32057  cvmsval  32058  frrlem1  32584  frrlem13  32596  neibastop1  33168  neibastop2lem  33169  neibastop2  33170  rdgssun  34036  isbnd  34448  ismndo2  34542  rngomndo  34603  isidl  34682  ispsubsp  36274  isnacs  38641  mzpclval  38662  elmzpcl  38663  mgmhmpropd  43360  issubmgm  43364  rnghmval  43466  zrrnghm  43492