Theorem raleqbi1dv 3333

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2755  df-ral 3081  df-rex 3091

This theorem is used by:  isoeq4  7338  frrlem1  8318  frrlem13  8330  smo11  8386  dffi2  9428  inficl  9430  dffi3  9436  dfom3  9661  aceq1  10209  dfac5lem4  10218  kmlem1  10242  kmlem10  10251  kmlem13  10254  kmlem14  10255  cofsmo  10360  infpssrlem4  10397  axdc3lem2  10542  elwina  10784  elina  10785  iswun  10802  eltskg  10848  elgrug  10890  elnp  11085  elnpi  11086  dfnn2  12361  dfnn3  12362  dfuzi  12803  coprmprod  16851  coprmproddvds  16853  ismri  17820  isprs  18485  isdrs  18490  ispos  18503  pospropd  18514  istos  18605  isdlat  18711  isipodrs  18726  mgmhmpropd  18902  issubmgm  18906  mhmpropd  19002  issubm  19013  subgacs  19386  nsgacs  19387  isghm  19445  ghmeql  19468  iscmn  20018  isomnd  20352  rnghmval  20685  dfrhm2  20719  zrrnghm  20803  isorng  21133  islss  21224  lssacs  21257  lmhmeql  21345  islbs  21366  lbsextlem1  21451  lbsextlem3  21453  lbsextlem4  21454  isobs  22041  mat0dimcrng  22800  istopg  23228  isbasisg  23280  basis2  23284  eltg2  23291  iscldtop  23428  neipeltop  23462  isreg  23665  regsep  23667  isnrm  23668  islly  23802  isnlly  23803  llyi  23808  nllyi  23809  islly2  23818  cldllycmp  23829  isfbas  24163  fbssfi  24171  isust  24538  elutop  24567  ustuqtop  24580  utopsnneip  24582  ispsmet  24638  ismet  24657  isxmet  24658  metrest  24858  cncfval  25224  fmcfil  25608  iscfil3  25609  caucfil  25619  iscmet3  25629  cfilres  25632  minveclem3  25765  wilthlem2  27411  wilthlem3  27412  wilth  27413  dfn0s2  28733  dfconngr1  30804  isconngr  30805  1conngr  30810  isplig  31093  isgrpo  31114  isablo  31163  disjabrex  33233  disjabrexf  33234  isrnsiga  34801  isldsys  34845  isros  34857  issros  34864  bnj1286  35705  bnj1452  35738  kur14lem9  36103  cvmscbv  36147  cvmsi  36154  cvmsval  36155  nmulprop  37069  neibastop1  37277  neibastop2lem  37278  neibastop2  37279  dfttc4lem1  37446  mh-inf3f1  37459  rdgssun  38444  isbnd  38857  ismndo2  38951  rngomndo  39012  isidl  39091  ispsubsp  40945  sn-isghm  43827  isnacs  43858  mzpclval  43879  elmzpcl  43880  relpeq4  46079  permac8prim  46146  nelsubc3lem  50326  isthinc  50696