Theorem rabeqdv 3484

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

Syntax hints:   → wi 4   = wceq 1533  {crab 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147

This theorem is referenced by:  rabeqbidv  3485  rabeqbidva  3486  rabsnif  4652  fvmptrabfv  6793  suppvalfn  7831  suppsnop  7838  fnsuppres  7851  pmvalg  8411  cantnffval  9120  hashbc  13805  elovmpowrd  13904  dfphi2  16105  mrisval  16895  coafval  17318  pmtrfval  18572  dprdval  19119  lspfval  19739  rrgval  20054  aspval  20096  mvrfval  20194  mhpfval  20326  dsmmbas2  20875  frlmbas  20893  clsfval  21627  ordtrest  21804  ordtrest2lem  21805  ordtrest2  21806  xkoval  22189  xkopt  22257  tsmsval2  22732  cncfval  23490  isphtpy  23579  cfilfval  23861  iscmet  23881  ttgval  26655  eengv  26759  isupgr  26863  upgrop  26873  isumgr  26874  upgrun  26897  umgrun  26899  isuspgr  26931  isusgr  26932  isuspgrop  26940  isusgrop  26941  isausgr  26943  ausgrusgrb  26944  usgrstrrepe  27011  lfuhgr1v0e  27030  usgrexmpl  27039  usgrexi  27217  cusgrsize  27230  1loopgrvd2  27279  wwlksn  27609  wspthsn  27620  iswwlksnon  27625  iswspthsnon  27628  clwwlknonmpo  27862  clwwlknon  27863  clwwlk0on0  27865  rmfsupp2  30861  ordtprsval  31156  snmlfval  32572  mpstval  32777  pclfvalN  37019  docaffvalN  38251  docafvalN  38252  etransclem11  42524  issmflem  42998  issmfd  43006  cnfsmf  43011  issmflelem  43015  issmfgtlem  43026  issmfgt  43027  issmfled  43028  issmfgtd  43031  issmfgelem  43039  fvmptrabdm  43486  prprspr2  43674  assintopmap  44107  dmatALTval  44449  rrxsphere  44729