Theorem rneqi 4985

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

Hypothesis

Ref	Expression
rneqi.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
rneqi	⊢ ran 𝐴 = ran 𝐵

Proof of Theorem rneqi

Step	Hyp	Ref	Expression
1		rneqi.1	. 2 ⊢ 𝐴 = 𝐵
2		rneq 4984	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 = ran 𝐵

Syntax hints:   = wceq 1398  ran crn 4750

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-in 3217  df-ss 3224  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110  df-opab 4172  df-cnv 4757  df-dm 4759  df-rn 4760

This theorem is referenced by:  rnmpt  5005  resima  5071  resima2  5072  mptima  5113  ima0  5121  rnuni  5174  imaundi  5175  imaundir  5176  inimass  5179  dminxp  5207  imainrect  5208  xpima1  5209  xpima2m  5210  rnresv  5222  imacnvcnv  5227  rnpropg  5242  imadmres  5255  mptpreima  5256  dmco  5271  resdif  5636  fpr  5866  fprg  5867  fliftfuns  5971  rnoprab  6136  rnmpo  6164  qliftfuns  6853  xpassen  7081  sbthlemi6  7232  ennnfonelemrn  13170  cnconst2  15098  elply2  15600  iedgedgg  16056  edgiedgbg  16060  edg0iedg0g  16061  uhgrvtxedgiedgb  16138  uspgrf1oedg  16171  usgrf1oedg  16200  usgredg3  16209  ushgredgedg  16221  ushgredgedgloop  16223  0grsubgr  16259  edginwlkd  16350