Theorem rabeqdv 3404

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

Syntax hints:   → wi 4   = wceq 1542  {crab 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390

This theorem is referenced by:  rabeqbidvaOLD  3406  rabsnif  4667  fvmptrabfv  6980  suppvalfng  8117  suppvalfn  8118  suppsnop  8128  fnsuppres  8141  pmvalg  8784  cantnffval  9584  hashbc  14415  elovmpowrd  14520  dfphi2  16744  mrisval  17596  coafval  18031  mndpsuppss  18733  pmtrfval  19425  dprdval  19980  rrgval  20674  lspfval  20968  lsppropd  21013  dsmmbas2  21717  frlmbas  21735  aspval  21852  mvrfval  21959  mhpfval  22104  psdffval  22123  clsfval  22990  ordtrest  23167  ordtrest2lem  23168  ordtrest2  23169  xkoval  23552  xkopt  23620  tsmsval2  24095  cncfval  24855  isphtpy  24948  cfilfval  25231  iscmet  25251  leftval  27841  rightval  27842  ttgval  28943  eengv  29048  isupgr  29153  upgrop  29163  isumgr  29164  upgrun  29187  umgrun  29189  isuspgr  29221  isusgr  29222  isuspgrop  29230  isusgrop  29231  isausgr  29233  ausgrusgrb  29234  usgrstrrepe  29304  lfuhgr1v0e  29323  usgrexi  29510  cusgrsize  29523  1loopgrvd2  29572  wwlksn  29905  wspthsn  29916  iswwlksnon  29921  iswspthsnon  29924  clwwlknonmpo  30159  clwwlknon  30160  clwwlk0on0  30162  fxpgaval  33228  rmfsupp2  33299  idlsrgval  33563  extvval  33675  splyval  33703  esplyval  33706  rspectopn  34011  zar0ring  34022  ordtprsval  34062  snmlfval  35512  mpstval  35717  pclfvalN  40335  docaffvalN  41567  docafvalN  41568  isprimroot  42532  dvnprodlem1  46374  etransclem11  46673  issmflem  47155  issmfd  47163  cnfsmf  47168  issmflelem  47172  issmfgtlem  47183  issmfgt  47184  issmfled  47185  issmfgtd  47189  issmfgelem  47197  fvmptrabdm  47741  prprspr2  47978  stgrusgra  48435  gpgusgra  48533  assintopmap  48682  dmatALTval  48876  rrxsphere  49224  initopropdlem  49715  termopropdlem  49716