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  9592  hashbc  14394  elovmpowrd  14499  dfphi2  16720  mrisval  17571  coafval  18006  mndpsuppss  18674  pmtrfval  19364  dprdval  19919  rrgval  20617  lspfval  20911  lsppropd  20957  dsmmbas2  21679  frlmbas  21697  aspval  21815  mvrfval  21923  mhpfval  22058  psdffval  22077  clsfval  22945  ordtrest  23122  ordtrest2lem  23123  ordtrest2  23124  xkoval  23507  xkopt  23575  tsmsval2  24050  cncfval  24814  isphtpy  24913  cfilfval  25197  iscmet  25217  leftval  27808  rightval  27809  ttgval  28855  eengv  28959  isupgr  29064  upgrop  29074  isumgr  29075  upgrun  29098  umgrun  29100  isuspgr  29132  isusgr  29133  isuspgrop  29141  isusgrop  29142  isausgr  29144  ausgrusgrb  29145  usgrstrrepe  29215  lfuhgr1v0e  29234  usgrexi  29421  cusgrsize  29435  1loopgrvd2  29484  wwlksn  29817  wspthsn  29828  iswwlksnon  29833  iswspthsnon  29836  clwwlknonmpo  30068  clwwlknon  30069  clwwlk0on0  30071  fxpgaval  33139  rmfsupp2  33205  idlsrgval  33467  rspectopn  33850  zar0ring  33861  ordtprsval  33901  snmlfval  35310  mpstval  35515  pclfvalN  39876  docaffvalN  41108  docafvalN  41109  isprimroot  42074  dvnprodlem1  45937  etransclem11  46236  issmflem  46718  issmfd  46726  cnfsmf  46731  issmflelem  46735  issmfgtlem  46746  issmfgt  46747  issmfled  46748  issmfgtd  46752  issmfgelem  46760  fvmptrabdm  47287  prprspr2  47512  stgrusgra  47951  gpgusgra  48041  assintopmap  48187  dmatALTval  48382  rrxsphere  48730  initopropdlem  49222  termopropdlem  49223