Theorem predeq3 6144

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

Syntax hints:   → wi 4   = wceq 1543  Predcpred 6139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-xp 5542  df-cnv 5544  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140

This theorem is referenced by:  dfpred3g  6151  predbrg  6160  preddowncl  6168  frpoinsg  6175  wfisg  6183  fpr3g  8004  frrlem1  8005  frrlem12  8016  frrlem13  8017  fpr2  8022  wfr3g  8031  wfrlem1  8032  wfrdmcl  8041  wfrlem14  8046  wfrlem15  8047  wfrlem17  8049  wfr2a  8050  trpredeq3  9305  trpredlem1  9310  trpredtr  9313  trpredmintr  9314  trpredrec  9320  frpoins3xpg  33457  frpoins3xp3g  33458  frmin  33459  frinsg  33462  xpord2pred  33472  sexp2  33473  xpord3pred  33478  sexp3  33479  elwlim  33497  frr3g  33504  frr2  33508  csbwrecsg  35184