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

Theorem predeq3 6255
Description: Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)
Assertion
Ref Expression
predeq3 (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))

Proof of Theorem predeq3
StepHypRef Expression
1 eqid 2737 . 2 𝑅 = 𝑅
2 eqid 2737 . 2 𝐴 = 𝐴
3 predeq123 6252 . 2 ((𝑅 = 𝑅𝐴 = 𝐴𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))
41, 2, 3mp3an12 1451 1 (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  Predcpred 6250
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5166  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6251
This theorem is referenced by:  dfpred3g  6263  predbrg  6273  preddowncl  6284  frpoinsg  6295  wfisgOLD  6306  frpoins3xpg  8064  frpoins3xp3g  8065  xpord2pred  8069  sexp2  8070  xpord3pred  8076  sexp3  8077  csbfrecsg  8207  fpr3g  8208  frrlem1  8209  frrlem12  8220  frrlem13  8221  fpr2a  8225  frrdmcl  8231  fprresex  8233  wfr3g  8245  wfrlem1OLD  8246  wfrdmclOLD  8255  wfrlem14OLD  8260  wfrlem15OLD  8261  wfrlem17OLD  8263  wfr2aOLD  8264  ttrclselem1  9619  ttrclselem2  9620  frmin  9643  frinsg  9645  frr3g  9650  frr2  9654  elwlim  34214
  Copyright terms: Public domain W3C validator