Theorem rneqi 5016

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

Hypothesis

Ref	Expression
rneqi.1	|- A = B

Assertion

Ref	Expression
rneqi	|- ran A = ran B

Proof of Theorem rneqi

Step	Hyp	Ref	Expression
1		rneqi.1	. 2 |- A = B
2		rneq 5015	. 2 |- ( A = B -> ran A = ran B )
3	1, 2	ax-mp 5	1 |- ran A = ran B

Syntax hints:   = wceq 1437   ran crn 4790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-rab 2717  df-v 3018  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3698  df-if 3848  df-sn 3935  df-pr 3937  df-op 3941  df-br 4360  df-opab 4419  df-cnv 4797  df-dm 4799  df-rn 4800

This theorem is referenced by:  rnmpt  5035  resima  5092  resima2  5093  ima0  5138  rnuni  5202  imaundi  5203  imaundir  5204  inimass  5207  dminxp  5232  imainrect  5233  xpima  5234  rnresv  5250  imacnvcnv  5255  rnpropg  5271  imadmres  5282  mptpreima  5283  dmco  5298  resdif  5787  fpr  6024  fliftfuns  6159  rnoprab  6330  rnmpt2  6357  elrnmpt2res  6361  curry1  6836  curry2  6839  fparlem3  6846  fparlem4  6847  qliftfuns  7398  xpassen  7612  sbthlem6  7633  hartogslem1  8003  rankwflemb  8209  fin23lem34  8720  axcc2lem  8810  axdc2lem  8822  fpwwe2lem13  9011  seqval  12167  0rest  15264  imasdsval2  15353  imasdsval2OLD  15365  fulloppc  15763  oppchofcl  16081  oyoncl  16091  gsumwspan  16566  pmtrprfvalrn  17065  psgnsn  17097  psgnprfval2  17100  oppglsm  17230  efgredlemg  17328  efgredlemd  17330  pf1rcl  18873  mpfpf1  18875  pf1ind  18879  pjdm  19205  leordtvallem1  20161  leordtvallem2  20162  leordtval  20164  cnconst2  20234  ptcmplem1  21002  tgpconcomp  21062  fmucndlem  21241  fmucnd  21242  ucnextcn  21254  metustto  21503  metustexhalf  21506  metuust  21510  cfilucfil2  21511  metuel  21514  psmetutop  21517  restmetu  21520  metucn  21521  minveclem5  22310  minvec  22313  minveclem5OLD  22322  minvecOLD  22325  ovolgelb  22368  ovoliunlem1  22390  itg1addlem4  22592  itg2seq  22635  itg2i1fseq  22648  itg2cnlem1  22654  efifo  23431  logrn  23443  dfrelog  23450  dvrelog  23517  xrlimcnp  23829  usgrares1  25073  cusgrares  25135  ex-rn  25825  rngoueqz  26093  zerdivemp1  26097  rngoridfz  26098  bafval  26158  cnnvba  26245  minveco  26461  minvecoOLD  26471  abrexexd  28079  imadifxp  28151  prsrn  28666  raddcn  28680  pl1cn  28706  esumrnmpt2  28834  sitgclbn  29121  mvtval  30083  elmsubrn  30111  ghomsn  30251  dfon4  30602  ellines  30861  rnmptsn  31638  f1omptsnlem  31639  icoreresf  31656  ptrest  31840  ovoliunnfl  31883  voliunnfl  31885  rngonegmn1l  32089  rngonegmn1r  32090  rngoneglmul  32091  rngonegrmul  32092  zerdivemp1x  32095  isdrngo2  32098  rngokerinj  32115  iscrngo2  32132  idlnegcl  32156  1idl  32160  0rngo  32161  smprngopr  32186  prnc  32201  isfldidl  32202  isdmn3  32208  mzpmfp  35495  dmnonrel  36103  imanonrel  36106  cnvrcl0  36139  rnresun  37346  disjinfi  37366  elicores  37520  ioodvbdlimc1lem1  37680  ioodvbdlimc1lem1OLD  37682  ioodvbdlimc1  37684  ioodvbdlimc2  37687  fourierdlem42  37889  fourierdlem42OLD  37890  sge0sn  38066  sge0split  38096  sge0fodjrnlem  38103  sge0xaddlem2  38121  volicorescl  38216  hoidmvlelem3  38260  uspgrf1oedg  39012  usgredg3  39037  iedgf1oedg  39047  usgredgedga  39048  usgrexmpledg  39068  0grsubgr  39081  uhgrspan1  39106  usgredgffibi  39120  dfnbgr3  39138  nbupgrres  39168  usgrnbcnvfv  39169  usgra2adedglem1  39255