Theorem rneqi 5937

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

Syntax hints:   = wceq 1542  ran crn 5678

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 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-cnv 5685  df-dm 5687  df-rn 5688

This theorem is referenced by:  rnmpt  5955  resima  6016  resima2  6017  mptima  6072  ima0  6077  rnuni  6149  imaundi  6150  imaundir  6151  inimass  6155  dminxp  6180  imainrect  6181  xpima  6182  rnresv  6201  imacnvcnv  6206  rnpropg  6222  imadmres  6234  mptpreima  6238  rnmpt0f  6243  dmco  6254  resdif  6855  fpr  7152  rnmptc  7208  fliftfuns  7311  rnoprab  7512  rnmpo  7542  elrnmpores  7546  curry1  8090  curry2  8093  fparlem3  8100  fparlem4  8101  fsplitfpar  8104  qliftfuns  8798  xpassen  9066  sbthlem6  9088  pwfir  9176  hartogslem1  9537  rnttrcl  9717  rankwflemb  9788  fin23lem34  10341  axcc2lem  10431  axdc2lem  10443  fpwwe2lem12  10637  seqval  13977  0rest  17375  imasdsval2  17462  fulloppc  17873  oppchofcl  18213  oyoncl  18223  gsumwspan  18727  pmtrprfvalrn  19356  psgnsn  19388  psgnprfval2  19391  oppglsm  19510  efgredlemg  19610  efgredlemd  19612  fincygsubgodd  19982  pjdm  21262  pf1rcl  21868  mpfpf1  21870  pf1ind  21874  leordtvallem1  22714  leordtvallem2  22715  leordtval  22717  cnconst2  22787  ptcmplem1  23556  tgpconncomp  23617  fmucndlem  23796  fmucnd  23797  ucnextcn  23809  metustto  24062  metustexhalf  24065  metuust  24069  cfilucfil2  24070  metuel  24073  psmetutop  24076  restmetu  24079  metucn  24080  minveclem5  24950  minvec  24953  ovolgelb  24997  ovoliunlem1  25019  itg1addlem4  25216  itg1addlem4OLD  25217  itg2seq  25260  itg2i1fseq  25273  itg2cnlem1  25279  efifo  26056  logrn  26067  dfrelog  26074  dvrelog  26145  xrlimcnp  26473  iedgedg  28310  edgiedgb  28314  edg0iedg0  28315  uhgrvtxedgiedgb  28396  uspgrf1oedg  28433  usgrf1oedg  28464  usgredg3  28473  ushgredgedg  28486  ushgredgedgloop  28488  usgrexmpledg  28519  0grsubgr  28535  uhgrspan1  28560  usgredgffibi  28581  dfnbgr3  28595  nbupgrres  28621  usgrnbcnvfv  28622  edginwlk  28892  wlkiswwlks2lem4  29126  wlkiswwlks2lem5  29127  clwlkclwwlk  29255  ex-rn  29693  bafval  29857  cnnvba  29932  minveco  30137  abrexexd  31746  imadifxp  31832  lsmsnorb  32501  prsrn  32895  raddcn  32909  pl1cn  32935  esumrnmpt2  33066  sitgclbn  33342  lfuhgr  34108  mvtval  34491  elmsubrn  34519  dfon4  34865  ellines  35124  rnmptsn  36216  f1omptsnlem  36217  icoreresf  36233  ptrest  36487  ovoliunnfl  36530  voliunnfl  36532  rngoueqz  36808  rngonegmn1l  36809  rngonegmn1r  36810  rngoneglmul  36811  rngonegrmul  36812  zerdivemp1x  36815  isdrngo2  36826  rngokerinj  36843  iscrngo2  36865  idlnegcl  36890  1idl  36894  0rngo  36895  smprngopr  36920  prnc  36935  isfldidl  36936  isdmn3  36942  rncnvepres  37172  imaopab  41050  mzpmfp  41485  dmnonrel  42341  imanonrel  42344  cnvrcl0  42376  ntrrn  42873  rnresun  43876  disjinfi  43891  imassmpt  43967  supxrleubrnmptf  44161  elicores  44246  limsupvaluz  44424  limsupmnflem  44436  limsupvaluz2  44454  limsup10ex  44489  liminf10ex  44490  liminflelimsuplem  44491  ioodvbdlimc1lem1  44647  ioodvbdlimc1  44649  ioodvbdlimc2  44651  fourierdlem42  44865  ioorrnopn  45021  subsaliuncl  45074  sge0sn  45095  sge0split  45125  sge0fodjrnlem  45132  sge0xaddlem2  45150  volicorescl  45269  hoidmvlelem3  45313  vonioolem2  45397  smflimsuplem1  45536  smflimsuplem3  45538  smflimsup  45544  fcoreslem2  45774