Theorem rabeqdv 3410

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

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

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 3395

This theorem is referenced by:  rabeqbidvaOLD  3412  rabsnif  4675  fvmptrabfv  6962  suppvalfng  8100  suppvalfn  8101  suppsnop  8111  fnsuppres  8124  pmvalg  8764  cantnffval  9559  hashbc  14360  elovmpowrd  14465  dfphi2  16685  mrisval  17536  coafval  17971  mndpsuppss  18639  pmtrfval  19329  dprdval  19884  rrgval  20582  lspfval  20876  lsppropd  20922  dsmmbas2  21644  frlmbas  21662  aspval  21780  mvrfval  21888  mhpfval  22023  psdffval  22042  clsfval  22910  ordtrest  23087  ordtrest2lem  23088  ordtrest2  23089  xkoval  23472  xkopt  23540  tsmsval2  24015  cncfval  24779  isphtpy  24878  cfilfval  25162  iscmet  25182  leftval  27775  rightval  27776  ttgval  28824  eengv  28928  isupgr  29033  upgrop  29043  isumgr  29044  upgrun  29067  umgrun  29069  isuspgr  29101  isusgr  29102  isuspgrop  29110  isusgrop  29111  isausgr  29113  ausgrusgrb  29114  usgrstrrepe  29184  lfuhgr1v0e  29203  usgrexi  29390  cusgrsize  29404  1loopgrvd2  29453  wwlksn  29786  wspthsn  29797  iswwlksnon  29802  iswspthsnon  29805  clwwlknonmpo  30037  clwwlknon  30038  clwwlk0on0  30040  fxpgaval  33118  rmfsupp2  33187  idlsrgval  33449  splyval  33561  rspectopn  33850  zar0ring  33861  ordtprsval  33901  snmlfval  35323  mpstval  35528  pclfvalN  39888  docaffvalN  41120  docafvalN  41121  isprimroot  42086  dvnprodlem1  45947  etransclem11  46246  issmflem  46728  issmfd  46736  cnfsmf  46741  issmflelem  46745  issmfgtlem  46756  issmfgt  46757  issmfled  46758  issmfgtd  46762  issmfgelem  46770  fvmptrabdm  47297  prprspr2  47522  stgrusgra  47963  gpgusgra  48061  assintopmap  48210  dmatALTval  48405  rrxsphere  48753  initopropdlem  49245  termopropdlem  49246