MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabeqdv Structured version   Visualization version   GIF version

Theorem rabeqdv 3423
Description: Equality of restricted class abstractions. Deduction form of rabeq 3422. (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
StepHypRef Expression
1 rabeqdv.1 . 2 (𝜑𝐴 = 𝐵)
2 rabeq 3422 . 2 (𝐴 = 𝐵 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
31, 2syl 17 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐵𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  {crab 3408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3409
This theorem is referenced by:  rabeqbidva  3424  rabsnif  4685  fvmptrabfv  6980  suppvalfng  8100  suppvalfn  8101  suppsnop  8110  fnsuppres  8123  pmvalg  8777  cantnffval  9600  hashbc  14351  elovmpowrd  14447  dfphi2  16647  mrisval  17511  coafval  17951  pmtrfval  19233  dprdval  19783  lspfval  20437  lsppropd  20482  rrgval  20760  dsmmbas2  21146  frlmbas  21164  aspval  21279  mvrfval  21392  mhpfval  21532  clsfval  22379  ordtrest  22556  ordtrest2lem  22557  ordtrest2  22558  xkoval  22941  xkopt  23009  tsmsval2  23484  cncfval  24254  isphtpy  24347  cfilfval  24631  iscmet  24651  leftval  27196  rightval  27197  ttgval  27820  ttgvalOLD  27821  eengv  27931  isupgr  28038  upgrop  28048  isumgr  28049  upgrun  28072  umgrun  28074  isuspgr  28106  isusgr  28107  isuspgrop  28115  isusgrop  28116  isausgr  28118  ausgrusgrb  28119  usgrstrrepe  28186  lfuhgr1v0e  28205  usgrexmpl  28214  usgrexi  28392  cusgrsize  28405  1loopgrvd2  28454  wwlksn  28785  wspthsn  28796  iswwlksnon  28801  iswspthsnon  28804  clwwlknonmpo  29036  clwwlknon  29037  clwwlk0on0  29039  rmfsupp2  32078  idlsrgval  32248  rspectopn  32451  zar0ring  32462  ordtprsval  32502  snmlfval  33927  mpstval  34132  pclfvalN  38355  docaffvalN  39587  docafvalN  39588  etransclem11  44493  issmflem  44975  issmfd  44983  cnfsmf  44988  issmflelem  44992  issmfgtlem  45003  issmfgt  45004  issmfled  45005  issmfgtd  45009  issmfgelem  45017  fvmptrabdm  45532  prprspr2  45717  assintopmap  46147  mndpsuppss  46454  dmatALTval  46488  rrxsphere  46841
  Copyright terms: Public domain W3C validator