Theorem rabeqdv 3437

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

Syntax hints:   → wi 4   = wceq 1567  {crab 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3423

This theorem is referenced by:  rabeqbidvaOLD  3439  rabsnif  4692  fvmptrabfv  7023  suppvalfng  8163  suppvalfn  8164  suppsnop  8174  fnsuppres  8187  pmvalg  8834  cantnffval  9632  hashbc  14490  elovmpowrd  14595  dfphi2  16833  mrisval  17686  coafval  18121  mndpsuppss  18823  pmtrfval  19520  dprdval  20075  rrgval  20782  lspfval  21072  lsppropd  21117  dsmmbas2  21856  frlmbas  21874  aspval  21991  mvrfval  22099  mhpfval  22270  psdffval  22289  clsfval  23151  ordtrest  23328  ordtrest2lem  23329  ordtrest2  23330  xkoval  23713  xkopt  23781  tsmsval2  24256  cncfval  25016  isphtpy  25109  cfilfval  25392  iscmet  25412  leftval  28008  rightval  28009  ttgval  29165  eengv  29270  isupgr  29375  upgrop  29385  isumgr  29386  upgrun  29409  umgrun  29411  isuspgr  29443  isusgr  29444  isuspgrop  29452  isusgrop  29453  isausgr  29455  ausgrusgrb  29456  usgrstrrepe  29526  lfuhgr1v0e  29545  usgrexi  29732  cusgrsize  29745  1loopgrvd2  29794  wwlksn  30127  wspthsn  30138  iswwlksnon  30143  iswspthsnon  30146  clwwlknonmpo  30381  clwwlknon  30382  clwwlk0on0  30384  fxpgaval  33428  rmfsupp2  33498  idlsrgval  33738  extvval  33866  splyval  33894  esplyval  33897  rspectopn  34202  zar0ring  34213  ordtprsval  34253  snmlfval  35755  mpstval  35960  pclfvalN  40588  docaffvalN  41820  docafvalN  41821  isprimroot  42785  dvnprodlem1  46587  etransclem11  46886  issmflem  47368  issmfd  47376  cnfsmf  47381  issmflelem  47385  issmfgtlem  47396  issmfgt  47397  issmfled  47398  issmfgtd  47402  issmfgelem  47410  fvmptrabdm  47954  prprspr2  48191  stgrusgra  48648  gpgusgra  48746  assintopmap  48895  dmatALTval  49100  rrxsphere  49448  initopropdlem  49938  termopropdlem  49939