Theorem rabeqdv 3427

Description: Equality of restricted class abstractions. Deduction form of rabeq 3426. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

Hypothesis

Ref	Expression
rabeqdv.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
rabeqdv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rabeqdv

Step	Hyp	Ref	Expression
1		rabeqdv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rabeq 3426	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3	1, 2	syl 18	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {crab 3412

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  rabsnif  4684  fvmptrabfv  7015  suppvalfng  8163  suppvalfn  8164  suppsnop  8174  fnsuppres  8187  pmvalg  8836  cantnffval  9642  hashbc  14551  elovmpowrd  14656  dfphi2  16898  mrisval  17751  coafval  18186  mndpsuppss  18906  pmtrfval  19611  dprdval  20166  rrgval  20896  lspfval  21195  lsppropd  21240  rspvalint  21470  dsmmbas2  21990  frlmbas  22008  aspval  22127  mvrfval  22235  mhpfval  22406  psdffval  22425  clsfval  23290  ordtrest  23467  ordtrest2lem  23468  ordtrest2  23469  xkoval  23853  xkopt  23921  tsmsval2  24396  cncfval  25156  isphtpy  25249  cfilfval  25532  iscmet  25552  leftval  28154  rightval  28155  angmgmval  29313  ttgval  29371  eengv  29476  isupgr  29581  upgrop  29591  isumgr  29592  upgrun  29615  umgrun  29617  isuspgr  29652  isusgr  29653  isuspgrop  29661  isusgrop  29662  isausgr  29664  ausgrusgrb  29665  usgrstrrepe  29735  lfuhgr1v0e  29754  usgrexi  29941  cusgrsize  29954  1loopgrvd2  30003  wwlksn  30345  wspthsn  30356  iswwlksnon  30361  iswspthsnon  30364  clwwlknonmpo  30599  clwwlknon  30600  clwwlk0on0  30602  fxpgaval  33647  rmfsupp2  33717  idlsrgval  33954  extvval  34082  splyval  34110  esplyval  34113  rspectopn  34418  zar0ring  34429  ordtprsval  34469  snmlfval  36010  mpstval  36215  pclfvalN  40860  docaffvalN  42092  docafvalN  42093  isprimroot  43057  dvnprodlem1  46872  etransclem11  47171  issmflem  47653  issmfd  47661  cnfsmf  47666  issmflelem  47670  issmfgtlem  47681  issmfgt  47682  issmfled  47683  issmfgtd  47687  issmfgelem  47695  fvmptrabdm  48279  prprspr2  48516  stgrusgra  48973  gpgusgra  49071  assintopmap  49219  dmatALTval  49428  rrxsphere  49776  initopropdlem  50264  termopropdlem  50265