Theorem rabeqdv 3486

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

Syntax hints:   → wi 4   = wceq 1537  {crab 3144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rab 3149

This theorem is referenced by:  rabeqbidv  3487  rabeqbidva  3488  rabsnif  4661  fvmptrabfv  6801  suppvalfn  7839  suppsnop  7846  fnsuppres  7859  pmvalg  8419  cantnffval  9128  hashbc  13814  elovmpowrd  13912  dfphi2  16113  mrisval  16903  coafval  17326  pmtrfval  18580  dprdval  19127  lspfval  19747  rrgval  20062  aspval  20104  mvrfval  20202  mhpfval  20334  dsmmbas2  20883  frlmbas  20901  clsfval  21635  ordtrest  21812  ordtrest2lem  21813  ordtrest2  21814  xkoval  22197  xkopt  22265  tsmsval2  22740  cncfval  23498  isphtpy  23587  cfilfval  23869  iscmet  23889  ttgval  26663  eengv  26767  isupgr  26871  upgrop  26881  isumgr  26882  upgrun  26905  umgrun  26907  isuspgr  26939  isusgr  26940  isuspgrop  26948  isusgrop  26949  isausgr  26951  ausgrusgrb  26952  usgrstrrepe  27019  lfuhgr1v0e  27038  usgrexmpl  27047  usgrexi  27225  cusgrsize  27238  1loopgrvd2  27287  wwlksn  27617  wspthsn  27628  iswwlksnon  27633  iswspthsnon  27636  clwwlknonmpo  27870  clwwlknon  27871  clwwlk0on0  27873  rmfsupp2  30868  ordtprsval  31163  snmlfval  32579  mpstval  32784  pclfvalN  37027  docaffvalN  38259  docafvalN  38260  etransclem11  42537  issmflem  43011  issmfd  43019  cnfsmf  43024  issmflelem  43028  issmfgtlem  43039  issmfgt  43040  issmfled  43041  issmfgtd  43044  issmfgelem  43052  fvmptrabdm  43499  prprspr2  43687  assintopmap  44120  dmatALTval  44462  rrxsphere  44742