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 1569  {crab 3412

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 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

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

This theorem is used by:  rabsnif  4683  fvmptrabfv  7026  suppvalfng  8184  suppvalfn  8185  suppsnop  8195  fnsuppres  8208  pmvalg  8857  cantnffval  9664  hashbc  14598  elovmpowrd  14703  dfphi2  16951  mrisval  17804  coafval  18239  mndpsuppss  18959  pmtrfval  19664  dprdval  20219  rrgval  20949  lspfval  21248  lsppropd  21293  rspvalint  21523  dsmmbas2  22043  frlmbas  22061  aspval  22180  mvrfval  22288  mhpfval  22459  psdffval  22478  clsfval  23343  ordtrest  23520  ordtrest2lem  23521  ordtrest2  23522  xkoval  23906  xkopt  23974  tsmsval2  24449  cncfval  25209  isphtpy  25302  cfilfval  25585  iscmet  25605  leftval  28235  rightval  28236  angmgmval  29394  ttgval  29452  eengv  29557  isupgr  29662  upgrop  29672  isumgr  29673  upgrun  29696  umgrun  29698  isuspgr  29733  isusgr  29734  isuspgrop  29742  isusgrop  29743  isausgr  29745  ausgrusgrb  29746  usgrstrrepe  29816  lfuhgr1v0e  29835  usgrexi  30022  cusgrsize  30035  1loopgrvd2  30084  wwlksn  30426  wspthsn  30437  iswwlksnon  30442  iswspthsnon  30445  clwwlknonmpo  30680  clwwlknon  30681  clwwlk0on0  30683  fxpgaval  33728  rmfsupp2  33798  idlsrgval  34035  extvval  34163  splyval  34191  esplyval  34194  rspectopn  34499  zar0ring  34510  ordtprsval  34550  snmlfval  36095  mpstval  36300  pclfvalN  40947  docaffvalN  42179  docafvalN  42180  isprimroot  43144  dvnprodlem1  46956  etransclem11  47255  issmflem  47737  issmfd  47745  cnfsmf  47750  issmflelem  47754  issmfgtlem  47765  issmfgt  47766  issmfled  47767  issmfgtd  47771  issmfgelem  47779  fvmptrabdm  48363  prprspr2  48600  stgrusgra  49057  gpgusgra  49155  assintopmap  49303  dmatALTval  49512  rrxsphere  49860  initopropdlem  50348  termopropdlem  50349