Theorem rneqi 5081

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 5080	. 2 |- ( A = B -> ran A = ran B )
3	1, 2	ax-mp 5	1 |- ran A = ran B

Syntax hints:   = wceq 1437   ran crn 4855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427  df-opab 4485  df-cnv 4862  df-dm 4864  df-rn 4865

This theorem is referenced by:  rnmpt  5100  resima  5157  resima2  5158  ima0  5203  rnuni  5267  imaundi  5268  imaundir  5269  inimass  5272  dminxp  5297  imainrect  5298  xpima  5299  rnresv  5315  imacnvcnv  5320  rnpropg  5336  imadmres  5347  mptpreima  5348  dmco  5363  resdif  5851  fpr  6087  fliftfuns  6222  rnoprab  6393  rnmpt2  6420  elrnmpt2res  6424  curry1  6899  curry2  6902  fparlem3  6909  fparlem4  6910  qliftfuns  7458  xpassen  7672  sbthlem6  7693  hartogslem1  8057  rankwflemb  8263  fin23lem34  8774  axcc2lem  8864  axdc2lem  8876  fpwwe2lem13  9066  seqval  12221  0rest  15287  imasdsval2  15373  fulloppc  15778  oppchofcl  16096  oyoncl  16106  gsumwspan  16581  pmtrprfvalrn  17080  psgnsn  17112  psgnprfval2  17115  oppglsm  17229  efgredlemg  17327  efgredlemd  17329  pf1rcl  18872  mpfpf1  18874  pf1ind  18878  pjdm  19201  leordtvallem1  20157  leordtvallem2  20158  leordtval  20160  cnconst2  20230  ptcmplem1  20998  tgpconcomp  21058  fmucndlem  21237  fmucnd  21238  ucnextcn  21250  metustto  21499  metustexhalf  21502  metuust  21506  cfilucfil2  21507  metuel  21510  psmetutop  21513  restmetu  21516  metucn  21517  minveclem5  22268  minvec  22271  ovolgelb  22311  ovoliunlem1  22333  itg1addlem4  22534  itg2seq  22577  itg2i1fseq  22590  itg2cnlem1  22596  efifo  23361  logrn  23373  dfrelog  23380  dvrelog  23447  xrlimcnp  23759  usgrares1  24983  cusgrares  25045  ex-rn  25735  rngoueqz  26003  zerdivemp1  26007  rngoridfz  26008  bafval  26068  cnnvba  26155  minveco  26371  abrexexd  27979  imadifxp  28051  prsrn  28560  raddcn  28574  pl1cn  28600  esumrnmpt2  28728  sitgclbn  29004  mvtval  29926  elmsubrn  29954  ghomsn  30094  dfon4  30445  ellines  30704  rnmptsn  31471  f1omptsnlem  31472  icoreresf  31489  ptrest  31643  ovoliunnfl  31686  voliunnfl  31688  rngonegmn1l  31892  rngonegmn1r  31893  rngoneglmul  31894  rngonegrmul  31895  zerdivemp1x  31898  isdrngo2  31901  rngokerinj  31918  iscrngo2  31935  idlnegcl  31959  1idl  31963  0rngo  31964  smprngopr  31989  prnc  32004  isfldidl  32005  isdmn3  32011  mzpmfp  35298  rnresun  37071  disjinfi  37091  ioodvbdlimc1lem1  37375  ioodvbdlimc1  37377  ioodvbdlimc2  37379  fourierdlem42  37580  sge0sn  37755  sge0split  37785  sge0fodjrnlem  37792  usgra2adedglem1  38426