Theorem rabeqdv 3409

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

Syntax hints:   → wi 4   = wceq 1539  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072

This theorem is referenced by:  rabeqbidv  3410  rabeqbidva  3411  rabsnif  4656  fvmptrabfv  6888  suppvalfng  7955  suppvalfn  7956  suppsnop  7965  fnsuppres  7978  pmvalg  8584  cantnffval  9351  hashbc  14093  elovmpowrd  14189  dfphi2  16403  mrisval  17256  coafval  17695  pmtrfval  18973  dprdval  19521  lspfval  20150  lsppropd  20195  rrgval  20471  dsmmbas2  20854  frlmbas  20872  aspval  20987  mvrfval  21099  mhpfval  21239  clsfval  22084  ordtrest  22261  ordtrest2lem  22262  ordtrest2  22263  xkoval  22646  xkopt  22714  tsmsval2  23189  cncfval  23957  isphtpy  24050  cfilfval  24333  iscmet  24353  ttgval  27140  eengv  27250  isupgr  27357  upgrop  27367  isumgr  27368  upgrun  27391  umgrun  27393  isuspgr  27425  isusgr  27426  isuspgrop  27434  isusgrop  27435  isausgr  27437  ausgrusgrb  27438  usgrstrrepe  27505  lfuhgr1v0e  27524  usgrexmpl  27533  usgrexi  27711  cusgrsize  27724  1loopgrvd2  27773  wwlksn  28103  wspthsn  28114  iswwlksnon  28119  iswspthsnon  28122  clwwlknonmpo  28354  clwwlknon  28355  clwwlk0on0  28357  rmfsupp2  31394  idlsrgval  31550  rspectopn  31719  zar0ring  31730  ordtprsval  31770  snmlfval  33192  mpstval  33397  leftval  33974  rightval  33975  pclfvalN  37830  docaffvalN  39062  docafvalN  39063  etransclem11  43676  issmflem  44150  issmfd  44158  cnfsmf  44163  issmflelem  44167  issmfgtlem  44178  issmfgt  44179  issmfled  44180  issmfgtd  44183  issmfgelem  44191  fvmptrabdm  44672  prprspr2  44858  assintopmap  45288  mndpsuppss  45595  dmatALTval  45629  rrxsphere  45982