Theorem predeq3 6261

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

Syntax hints:   → wi 4   = wceq 1541  Predcpred 6256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097  df-opab 5159  df-xp 5628  df-cnv 5630  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257

This theorem is referenced by:  dfpred3g  6269  preddowncl  6288  frpoinsg  6299  frpoins3xpg  8080  frpoins3xp3g  8081  xpord2pred  8085  sexp2  8086  xpord3pred  8092  sexp3  8093  csbfrecsg  8224  fpr3g  8225  frrlem1  8226  frrlem12  8237  frrlem13  8238  fpr2a  8242  frrdmcl  8248  fprresex  8250  wfr3g  8259  ttrclselem1  9632  ttrclselem2  9633  frmin  9659  frinsg  9661  frr3g  9666  frr2  9670  elwlim  35964