Theorem rneqi 5807

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 5806	. 2 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 = ran 𝐵

Syntax hints:   = wceq 1537  ran crn 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-cnv 5563  df-dm 5565  df-rn 5566

This theorem is referenced by:  rnmpt  5827  resima  5887  resima2  5888  mptima  5941  ima0  5945  rnuni  6007  imaundi  6008  imaundir  6009  inimass  6012  dminxp  6037  imainrect  6038  xpima  6039  rnresv  6058  imacnvcnv  6063  rnpropg  6079  imadmres  6091  mptpreima  6092  dmco  6107  resdif  6635  fpr  6916  rnmptc  6969  fliftfuns  7067  rnoprab  7257  rnmpo  7284  elrnmpores  7288  curry1  7799  curry2  7802  fparlem3  7809  fparlem4  7810  fsplitfpar  7814  qliftfuns  8384  xpassen  8611  sbthlem6  8632  hartogslem1  9006  rankwflemb  9222  fin23lem34  9768  axcc2lem  9858  axdc2lem  9870  fpwwe2lem13  10064  seqval  13381  0rest  16703  imasdsval2  16789  fulloppc  17192  oppchofcl  17510  oyoncl  17520  gsumwspan  18011  pmtrprfvalrn  18616  psgnsn  18648  psgnprfval2  18651  oppglsm  18767  efgredlemg  18868  efgredlemd  18870  fincygsubgodd  19234  pf1rcl  20512  mpfpf1  20514  pf1ind  20518  pjdm  20851  leordtvallem1  21818  leordtvallem2  21819  leordtval  21821  cnconst2  21891  ptcmplem1  22660  tgpconncomp  22721  fmucndlem  22900  fmucnd  22901  ucnextcn  22913  metustto  23163  metustexhalf  23166  metuust  23170  cfilucfil2  23171  metuel  23174  psmetutop  23177  restmetu  23180  metucn  23181  minveclem5  24036  minvec  24039  ovolgelb  24081  ovoliunlem1  24103  itg1addlem4  24300  itg2seq  24343  itg2i1fseq  24356  itg2cnlem1  24362  efifo  25131  logrn  25142  dfrelog  25149  dvrelog  25220  xrlimcnp  25546  iedgedg  26835  edgiedgb  26839  edg0iedg0  26840  uhgrvtxedgiedgb  26921  uspgrf1oedg  26958  usgrf1oedg  26989  usgredg3  26998  ushgredgedg  27011  ushgredgedgloop  27013  usgrexmpledg  27044  0grsubgr  27060  uhgrspan1  27085  usgredgffibi  27106  dfnbgr3  27120  nbupgrres  27146  usgrnbcnvfv  27147  edginwlk  27416  wlkiswwlks2lem4  27650  wlkiswwlks2lem5  27651  clwlkclwwlk  27780  ex-rn  28219  bafval  28381  cnnvba  28456  minveco  28661  abrexexd  30269  imadifxp  30351  lsmsnorb  30945  prsrn  31158  raddcn  31172  pl1cn  31198  esumrnmpt2  31327  sitgclbn  31601  lfuhgr  32364  mvtval  32747  elmsubrn  32775  dfon4  33354  ellines  33613  rnmptsn  34619  f1omptsnlem  34620  icoreresf  34636  ptrest  34906  ovoliunnfl  34949  voliunnfl  34951  rngoueqz  35233  rngonegmn1l  35234  rngonegmn1r  35235  rngoneglmul  35236  rngonegrmul  35237  zerdivemp1x  35240  isdrngo2  35251  rngokerinj  35268  iscrngo2  35290  idlnegcl  35315  1idl  35319  0rngo  35320  smprngopr  35345  prnc  35360  isfldidl  35361  isdmn3  35367  rncnvepres  35576  imaopab  39168  mzpmfp  39393  dmnonrel  39999  imanonrel  40002  cnvrcl0  40034  ntrrn  40521  rnresun  41485  disjinfi  41503  rnmpt0  41532  imassmpt  41586  supxrleubrnmptf  41776  elicores  41858  limsupvaluz  42038  limsupmnflem  42050  limsupvaluz2  42068  limsup10ex  42103  liminf10ex  42104  liminflelimsuplem  42105  ioodvbdlimc1lem1  42265  ioodvbdlimc1  42267  ioodvbdlimc2  42269  fourierdlem42  42483  ioorrnopn  42639  subsaliuncl  42690  sge0sn  42710  sge0split  42740  sge0fodjrnlem  42747  sge0xaddlem2  42765  volicorescl  42884  hoidmvlelem3  42928  vonioolem2  43012  smflimsuplem1  43143  smflimsuplem3  43145  smflimsup  43151