Theorem rabeqdv 3419

Description: Equality of restricted class abstractions. Deduction form of rabeq 3418. (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 3418	. 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})

Syntax hints:   → wi 4   = wceq 1539  {crab 3068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073

This theorem is referenced by:  rabeqbidv  3420  rabeqbidva  3421  rabsnif  4659  fvmptrabfv  6906  suppvalfng  7984  suppvalfn  7985  suppsnop  7994  fnsuppres  8007  pmvalg  8626  cantnffval  9421  hashbc  14165  elovmpowrd  14261  dfphi2  16475  mrisval  17339  coafval  17779  pmtrfval  19058  dprdval  19606  lspfval  20235  lsppropd  20280  rrgval  20558  dsmmbas2  20944  frlmbas  20962  aspval  21077  mvrfval  21189  mhpfval  21329  clsfval  22176  ordtrest  22353  ordtrest2lem  22354  ordtrest2  22355  xkoval  22738  xkopt  22806  tsmsval2  23281  cncfval  24051  isphtpy  24144  cfilfval  24428  iscmet  24448  ttgval  27236  ttgvalOLD  27237  eengv  27347  isupgr  27454  upgrop  27464  isumgr  27465  upgrun  27488  umgrun  27490  isuspgr  27522  isusgr  27523  isuspgrop  27531  isusgrop  27532  isausgr  27534  ausgrusgrb  27535  usgrstrrepe  27602  lfuhgr1v0e  27621  usgrexmpl  27630  usgrexi  27808  cusgrsize  27821  1loopgrvd2  27870  wwlksn  28202  wspthsn  28213  iswwlksnon  28218  iswspthsnon  28221  clwwlknonmpo  28453  clwwlknon  28454  clwwlk0on0  28456  rmfsupp2  31492  idlsrgval  31648  rspectopn  31817  zar0ring  31828  ordtprsval  31868  snmlfval  33292  mpstval  33497  leftval  34047  rightval  34048  pclfvalN  37903  docaffvalN  39135  docafvalN  39136  etransclem11  43786  issmflem  44263  issmfd  44271  cnfsmf  44276  issmflelem  44280  issmfgtlem  44291  issmfgt  44292  issmfled  44293  issmfgtd  44296  issmfgelem  44304  fvmptrabdm  44785  prprspr2  44970  assintopmap  45400  mndpsuppss  45707  dmatALTval  45741  rrxsphere  46094