Theorem rabeqdv 3418

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

Syntax hints:   → wi 4   = wceq 1540  {crab 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403

This theorem is referenced by:  rabeqbidvaOLD  3420  rabsnif  4683  fvmptrabfv  6982  suppvalfng  8123  suppvalfn  8124  suppsnop  8134  fnsuppres  8147  pmvalg  8787  cantnffval  9594  hashbc  14396  elovmpowrd  14501  dfphi2  16721  mrisval  17572  coafval  18007  mndpsuppss  18675  pmtrfval  19365  dprdval  19920  rrgval  20618  lspfval  20912  lsppropd  20958  dsmmbas2  21680  frlmbas  21698  aspval  21816  mvrfval  21924  mhpfval  22059  psdffval  22078  clsfval  22946  ordtrest  23123  ordtrest2lem  23124  ordtrest2  23125  xkoval  23508  xkopt  23576  tsmsval2  24051  cncfval  24815  isphtpy  24914  cfilfval  25198  iscmet  25218  leftval  27809  rightval  27810  ttgval  28856  eengv  28960  isupgr  29065  upgrop  29075  isumgr  29076  upgrun  29099  umgrun  29101  isuspgr  29133  isusgr  29134  isuspgrop  29142  isusgrop  29143  isausgr  29145  ausgrusgrb  29146  usgrstrrepe  29216  lfuhgr1v0e  29235  usgrexi  29422  cusgrsize  29436  1loopgrvd2  29485  wwlksn  29818  wspthsn  29829  iswwlksnon  29834  iswspthsnon  29837  clwwlknonmpo  30069  clwwlknon  30070  clwwlk0on0  30072  fxpgaval  33140  rmfsupp2  33206  idlsrgval  33468  rspectopn  33851  zar0ring  33862  ordtprsval  33902  snmlfval  35311  mpstval  35516  pclfvalN  39877  docaffvalN  41109  docafvalN  41110  isprimroot  42075  dvnprodlem1  45938  etransclem11  46237  issmflem  46719  issmfd  46727  cnfsmf  46732  issmflelem  46736  issmfgtlem  46747  issmfgt  46748  issmfled  46749  issmfgtd  46753  issmfgelem  46761  fvmptrabdm  47288  prprspr2  47513  stgrusgra  47952  gpgusgra  48042  assintopmap  48188  dmatALTval  48383  rrxsphere  48731  initopropdlem  49223  termopropdlem  49224