Theorem predeq3 6303

Description: Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.)

Assertion

Ref	Expression
predeq3	⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))

Proof of Theorem predeq3

Step	Hyp	Ref	Expression
1		eqid 2730	. 2 ⊢ 𝑅 = 𝑅
2		eqid 2730	. 2 ⊢ 𝐴 = 𝐴
3		predeq123 6300	. 2 ⊢ ((𝑅 = 𝑅 ∧ 𝐴 = 𝐴 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))
4	1, 2, 3	mp3an12 1449	1 ⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))

Syntax hints:   → wi 4   = wceq 1539  Predcpred 6298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299

This theorem is referenced by:  dfpred3g  6311  predbrg  6321  preddowncl  6332  frpoinsg  6343  wfisgOLD  6354  frpoins3xpg  8128  frpoins3xp3g  8129  xpord2pred  8133  sexp2  8134  xpord3pred  8140  sexp3  8141  csbfrecsg  8271  fpr3g  8272  frrlem1  8273  frrlem12  8284  frrlem13  8285  fpr2a  8289  frrdmcl  8295  fprresex  8297  wfr3g  8309  wfrlem1OLD  8310  wfrdmclOLD  8319  wfrlem14OLD  8324  wfrlem15OLD  8325  wfrlem17OLD  8327  wfr2aOLD  8328  ttrclselem1  9722  ttrclselem2  9723  frmin  9746  frinsg  9748  frr3g  9753  frr2  9757  elwlim  35099