Theorem raleqbi1dv 3329

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

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

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 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ral 3077  df-rex 3087

This theorem is used by:  isoeq4  7322  frrlem1  8286  frrlem13  8298  smo11  8354  dffi2  9396  inficl  9398  dffi3  9404  dfom3  9629  aceq1  10123  dfac5lem4  10132  kmlem1  10156  kmlem10  10165  kmlem13  10168  kmlem14  10169  cofsmo  10274  infpssrlem4  10311  axdc3lem2  10456  elwina  10698  elina  10699  iswun  10716  eltskg  10762  elgrug  10804  elnp  10999  elnpi  11000  dfnn2  12273  dfnn3  12274  dfuzi  12715  coprmprod  16754  coprmproddvds  16756  ismri  17722  isprs  18387  isdrs  18392  ispos  18405  pospropd  18416  istos  18507  isdlat  18613  isipodrs  18628  mgmhmpropd  18803  issubmgm  18807  mhmpropd  18903  issubm  18914  subgacs  19287  nsgacs  19288  isghm  19346  ghmeql  19369  iscmn  19919  isomnd  20253  rnghmval  20584  dfrhm2  20618  zrrnghm  20701  isorng  21030  islss  21121  lssacs  21154  lmhmeql  21242  islbs  21263  lbsextlem1  21348  lbsextlem3  21350  lbsextlem4  21351  isobs  21936  mat0dimcrng  22695  istopg  23123  isbasisg  23175  basis2  23179  eltg2  23186  iscldtop  23323  neipeltop  23357  isreg  23560  regsep  23562  isnrm  23563  islly  23697  isnlly  23698  llyi  23703  nllyi  23704  islly2  23713  cldllycmp  23724  isfbas  24058  fbssfi  24066  isust  24433  elutop  24462  ustuqtop  24475  utopsnneip  24477  ispsmet  24533  ismet  24552  isxmet  24553  metrest  24753  cncfval  25119  fmcfil  25503  iscfil3  25504  caucfil  25514  iscmet3  25524  cfilres  25527  minveclem3  25660  wilthlem2  27308  wilthlem3  27309  wilth  27310  dfn0s2  28600  dfconngr1  30671  isconngr  30672  1conngr  30677  isplig  30960  isgrpo  30981  isablo  31030  disjabrex  33058  disjabrexf  33059  isrnsiga  34626  isldsys  34670  isros  34682  issros  34689  bnj1286  35531  bnj1452  35564  kur14lem9  35796  cvmscbv  35840  cvmsi  35847  cvmsval  35848  nmulprop  36773  neibastop1  36981  neibastop2lem  36982  neibastop2  36983  dfttc4lem1  37150  mh-inf3f1  37163  rdgssun  38135  isbnd  38533  ismndo2  38627  rngomndo  38688  isidl  38767  ispsubsp  40621  sn-isghm  43522  isnacs  43552  mzpclval  43573  elmzpcl  43574  relpeq4  45773  permac8prim  45840  nelsubc3lem  49999  isthinc  50348