Theorem rneqd 4952

Description: Equality deduction for range. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
rneqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
rneqd	⊢ (𝜑 → ran 𝐴 = ran 𝐵)

Proof of Theorem rneqd

Step	Hyp	Ref	Expression
1		rneqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rneq 4950	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1395  ran crn 4719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-in 3203  df-ss 3210  df-sn 3672  df-pr 3673  df-op 3675  df-br 4083  df-opab 4145  df-cnv 4726  df-dm 4728  df-rn 4729

This theorem is referenced by:  resima2  5038  imaeq1  5062  imaeq2  5063  mptimass  5080  resiima  5085  elxp4  5215  elxp5  5216  funimacnv  5396  funimaexg  5404  fnima  5441  fnrnfv  5679  2ndvalg  6287  fo2nd  6302  f2ndres  6304  en1  6949  xpassen  6985  xpdom2  6986  sbthlemi4  7123  djudom  7256  exmidfodomrlemim  7375  seqeq1  10667  seqeq2  10668  seqeq3  10669  seq3val  10677  seqvalcd  10678  s1rn  11146  ennnfonelemex  12980  ennnfonelemf1  12984  restval  13273  restid2  13276  prdsex  13297  prdsval  13301  imasival  13334  conjsubg  13809  rnrhmsubrg  14210  tgrest  14837  txvalex  14922  txval  14923  mopnval  15110  edgvalg  15854  edgopval  15856  edgstruct  15858  uhgr2edg  15998