Theorem rabeqdv 3452

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437

This theorem is referenced by:  rabeqbidvaOLD  3454  rabsnif  4723  fvmptrabfv  7048  suppvalfng  8192  suppvalfn  8193  suppsnop  8203  fnsuppres  8216  pmvalg  8877  cantnffval  9703  hashbc  14492  elovmpowrd  14596  dfphi2  16811  mrisval  17673  coafval  18109  mndpsuppss  18778  pmtrfval  19468  dprdval  20023  rrgval  20697  lspfval  20971  lsppropd  21017  dsmmbas2  21757  frlmbas  21775  aspval  21893  mvrfval  22001  mhpfval  22142  psdffval  22161  clsfval  23033  ordtrest  23210  ordtrest2lem  23211  ordtrest2  23212  xkoval  23595  xkopt  23663  tsmsval2  24138  cncfval  24914  isphtpy  25013  cfilfval  25298  iscmet  25318  leftval  27902  rightval  27903  ttgval  28883  ttgvalOLD  28884  eengv  28994  isupgr  29101  upgrop  29111  isumgr  29112  upgrun  29135  umgrun  29137  isuspgr  29169  isusgr  29170  isuspgrop  29178  isusgrop  29179  isausgr  29181  ausgrusgrb  29182  usgrstrrepe  29252  lfuhgr1v0e  29271  usgrexi  29458  cusgrsize  29472  1loopgrvd2  29521  wwlksn  29857  wspthsn  29868  iswwlksnon  29873  iswspthsnon  29876  clwwlknonmpo  30108  clwwlknon  30109  clwwlk0on0  30111  rmfsupp2  33242  idlsrgval  33531  rspectopn  33866  zar0ring  33877  ordtprsval  33917  snmlfval  35335  mpstval  35540  pclfvalN  39891  docaffvalN  41123  docafvalN  41124  isprimroot  42094  dvnprodlem1  45961  etransclem11  46260  issmflem  46742  issmfd  46750  cnfsmf  46755  issmflelem  46759  issmfgtlem  46770  issmfgt  46771  issmfled  46772  issmfgtd  46776  issmfgelem  46784  fvmptrabdm  47305  prprspr2  47505  stgrusgra  47926  gpgusgra  48012  assintopmap  48122  dmatALTval  48317  rrxsphere  48669