Theorem rneqi 5931

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

Syntax hints:   = wceq 1542  ran crn 5673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5145  df-opab 5207  df-cnv 5680  df-dm 5682  df-rn 5683

This theorem is referenced by:  rnmpt  5949  resima  6010  resima2  6011  mptima  6064  ima0  6068  rnuni  6140  imaundi  6141  imaundir  6142  inimass  6146  dminxp  6171  imainrect  6172  xpima  6173  rnresv  6192  imacnvcnv  6197  rnpropg  6213  imadmres  6225  mptpreima  6229  rnmpt0f  6234  dmco  6245  resdif  6844  fpr  7139  rnmptc  7195  fliftfuns  7298  rnoprab  7499  rnmpo  7529  elrnmpores  7533  curry1  8077  curry2  8080  fparlem3  8087  fparlem4  8088  fsplitfpar  8091  qliftfuns  8786  xpassen  9054  sbthlem6  9076  pwfir  9164  hartogslem1  9524  rnttrcl  9704  rankwflemb  9775  fin23lem34  10328  axcc2lem  10418  axdc2lem  10430  fpwwe2lem12  10624  seqval  13964  0rest  17362  imasdsval2  17449  fulloppc  17860  oppchofcl  18200  oyoncl  18210  gsumwspan  18714  pmtrprfvalrn  19340  psgnsn  19372  psgnprfval2  19375  oppglsm  19494  efgredlemg  19594  efgredlemd  19596  fincygsubgodd  19965  pjdm  21235  pf1rcl  21837  mpfpf1  21839  pf1ind  21843  leordtvallem1  22683  leordtvallem2  22684  leordtval  22686  cnconst2  22756  ptcmplem1  23525  tgpconncomp  23586  fmucndlem  23765  fmucnd  23766  ucnextcn  23778  metustto  24031  metustexhalf  24034  metuust  24038  cfilucfil2  24039  metuel  24042  psmetutop  24045  restmetu  24048  metucn  24049  minveclem5  24919  minvec  24922  ovolgelb  24966  ovoliunlem1  24988  itg1addlem4  25185  itg1addlem4OLD  25186  itg2seq  25229  itg2i1fseq  25242  itg2cnlem1  25248  efifo  26025  logrn  26036  dfrelog  26043  dvrelog  26114  xrlimcnp  26440  iedgedg  28277  edgiedgb  28281  edg0iedg0  28282  uhgrvtxedgiedgb  28363  uspgrf1oedg  28400  usgrf1oedg  28431  usgredg3  28440  ushgredgedg  28453  ushgredgedgloop  28455  usgrexmpledg  28486  0grsubgr  28502  uhgrspan1  28527  usgredgffibi  28548  dfnbgr3  28562  nbupgrres  28588  usgrnbcnvfv  28589  edginwlk  28859  wlkiswwlks2lem4  29093  wlkiswwlks2lem5  29094  clwlkclwwlk  29222  ex-rn  29660  bafval  29822  cnnvba  29897  minveco  30102  abrexexd  31711  imadifxp  31798  lsmsnorb  32459  prsrn  32826  raddcn  32840  pl1cn  32866  esumrnmpt2  32997  sitgclbn  33273  lfuhgr  34039  mvtval  34422  elmsubrn  34450  dfon4  34796  ellines  35055  rnmptsn  36121  f1omptsnlem  36122  icoreresf  36138  ptrest  36392  ovoliunnfl  36435  voliunnfl  36437  rngoueqz  36714  rngonegmn1l  36715  rngonegmn1r  36716  rngoneglmul  36717  rngonegrmul  36718  zerdivemp1x  36721  isdrngo2  36732  rngokerinj  36749  iscrngo2  36771  idlnegcl  36796  1idl  36800  0rngo  36801  smprngopr  36826  prnc  36841  isfldidl  36842  isdmn3  36848  rncnvepres  37078  imaopab  40967  mzpmfp  41356  dmnonrel  42212  imanonrel  42215  cnvrcl0  42247  ntrrn  42744  rnresun  43747  disjinfi  43762  imassmpt  43840  supxrleubrnmptf  44034  elicores  44119  limsupvaluz  44297  limsupmnflem  44309  limsupvaluz2  44327  limsup10ex  44362  liminf10ex  44363  liminflelimsuplem  44364  ioodvbdlimc1lem1  44520  ioodvbdlimc1  44522  ioodvbdlimc2  44524  fourierdlem42  44738  ioorrnopn  44894  subsaliuncl  44947  sge0sn  44968  sge0split  44998  sge0fodjrnlem  45005  sge0xaddlem2  45023  volicorescl  45142  hoidmvlelem3  45186  vonioolem2  45270  smflimsuplem1  45409  smflimsuplem3  45411  smflimsup  45417  fcoreslem2  45647