Theorem predeq3 6278

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

Syntax hints:   → wi 4   = wceq 1540  Predcpred 6273

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274

This theorem is referenced by:  dfpred3g  6286  preddowncl  6305  frpoinsg  6316  frpoins3xpg  8119  frpoins3xp3g  8120  xpord2pred  8124  sexp2  8125  xpord3pred  8131  sexp3  8132  csbfrecsg  8263  fpr3g  8264  frrlem1  8265  frrlem12  8276  frrlem13  8277  fpr2a  8281  frrdmcl  8287  fprresex  8289  wfr3g  8298  ttrclselem1  9678  ttrclselem2  9679  frmin  9702  frinsg  9704  frr3g  9709  frr2  9713  elwlim  35811