Theorem predeq3 6309

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 2728	. 2 ⊢ 𝑅 = 𝑅
2		eqid 2728	. 2 ⊢ 𝐴 = 𝐴
3		predeq123 6306	. 2 ⊢ ((𝑅 = 𝑅 ∧ 𝐴 = 𝐴 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))
4	1, 2, 3	mp3an12 1448	1 ⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌))

Syntax hints:   → wi 4   = wceq 1534  Predcpred 6304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3430  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5149  df-opab 5211  df-xp 5684  df-cnv 5686  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305

This theorem is referenced by:  dfpred3g  6317  predbrg  6327  preddowncl  6338  frpoinsg  6349  wfisgOLD  6360  frpoins3xpg  8145  frpoins3xp3g  8146  xpord2pred  8150  sexp2  8151  xpord3pred  8157  sexp3  8158  csbfrecsg  8290  fpr3g  8291  frrlem1  8292  frrlem12  8303  frrlem13  8304  fpr2a  8308  frrdmcl  8314  fprresex  8316  wfr3g  8328  wfrlem1OLD  8329  wfrdmclOLD  8338  wfrlem14OLD  8343  wfrlem15OLD  8344  wfrlem17OLD  8346  wfr2aOLD  8347  ttrclselem1  9749  ttrclselem2  9750  frmin  9773  frinsg  9775  frr3g  9780  frr2  9784  elwlim  35419