Theorem rabeqdv 3429

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {crab 3414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415

This theorem is used by:  rabeqbidvaOLD  3431  rabsnif  4687  fvmptrabfv  7023  suppvalfng  8168  suppvalfn  8169  suppsnop  8179  fnsuppres  8192  pmvalg  8839  cantnffval  9645  hashbc  14520  elovmpowrd  14625  dfphi2  16869  mrisval  17722  coafval  18157  mndpsuppss  18874  pmtrfval  19578  dprdval  20133  rrgval  20860  lspfval  21158  lsppropd  21203  rspvalint  21433  dsmmbas2  21951  frlmbas  21969  aspval  22088  mvrfval  22196  mhpfval  22367  psdffval  22386  clsfval  23251  ordtrest  23428  ordtrest2lem  23429  ordtrest2  23430  xkoval  23814  xkopt  23882  tsmsval2  24357  cncfval  25117  isphtpy  25210  cfilfval  25493  iscmet  25513  leftval  28112  rightval  28113  ttgval  29317  eengv  29422  isupgr  29527  upgrop  29537  isumgr  29538  upgrun  29561  umgrun  29563  isuspgr  29598  isusgr  29599  isuspgrop  29607  isusgrop  29608  isausgr  29610  ausgrusgrb  29611  usgrstrrepe  29681  lfuhgr1v0e  29700  usgrexi  29887  cusgrsize  29900  1loopgrvd2  29949  wwlksn  30291  wspthsn  30302  iswwlksnon  30307  iswspthsnon  30310  clwwlknonmpo  30545  clwwlknon  30546  clwwlk0on0  30548  fxpgaval  33594  rmfsupp2  33664  idlsrgval  33900  extvval  34028  splyval  34056  esplyval  34059  rspectopn  34364  zar0ring  34375  ordtprsval  34415  snmlfval  35896  mpstval  36101  pclfvalN  40749  docaffvalN  41981  docafvalN  41982  isprimroot  42946  dvnprodlem1  46761  etransclem11  47060  issmflem  47542  issmfd  47550  cnfsmf  47555  issmflelem  47559  issmfgtlem  47570  issmfgt  47571  issmfled  47572  issmfgtd  47576  issmfgelem  47584  fvmptrabdm  48168  prprspr2  48405  stgrusgra  48862  gpgusgra  48960  assintopmap  49108  dmatALTval  49317  rrxsphere  49665  initopropdlem  50153  termopropdlem  50154