Theorem rneqi 5919

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

This proof depends on syntax axioms:   = wceq 1570  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  rnmpt  5939  resima  6056  resima2  6057  mptima  6070  ima0  6075  rnuni  6140  imaundi  6141  imaundir  6142  inimass  6145  dminxp  6172  imainrect  6173  xpima  6174  rnresv  6195  imadifssranOLD  6202  imacnvcnv  6207  rnpropg  6223  imadmres  6235  mptpreima  6239  rnmpt0f  6244  dmco  6256  resdif  6846  fpr  7158  rnmptc  7213  fliftfuns  7322  rnoprab  7525  rnmpo  7553  elrnmpores  7558  curry1  8115  curry2  8118  fparlem3  8125  fparlem4  8126  fsplitfpar  8129  qliftfuns  8825  xpassen  9090  sbthlem6  9111  pwfir  9308  hartogslem1  9536  rnttrcl  9723  rankwflembOLD  9801  fin23lem34  10424  axcc2lem  10514  axdc2lem  10526  fpwwe2lem12  10727  seqval  14155  0rest  17600  imasdsval2  17688  fulloppc  18099  oppchofcl  18434  oyoncl  18444  gsumwspan  19042  pmtrprfvalrn  19702  psgnsn  19734  psgnprfval2  19737  oppglsm  19856  efgredlemg  19956  efgredlemd  19958  fincygsubgodd  20328  pjdm  22013  pf1rcl  22667  mpfpf1  22669  pf1ind  22673  leordtvallem1  23528  leordtvallem2  23529  leordtval  23531  cnconst2  23601  ptcmplem1  24371  tgpconncomp  24432  fmucndlem  24609  fmucnd  24610  ucnextcn  24622  metustto  24872  metustexhalf  24875  metuust  24879  cfilucfil2  24880  metuel  24883  psmetutop  24886  restmetu  24889  metucn  24890  minveclem5  25754  minvec  25757  ovolgelb  25801  ovoliunlem1  25823  itg1addlem4  26020  itg2seq  26063  itg2i1fseq  26076  itg2cnlem1  26082  efifo  26875  logrn  26886  dfrelog  26893  dvrelog  26965  xrlimcnp  27296  iedgedg  29628  edgiedgb  29632  edg0iedg0  29633  uhgrvtxedgiedgb  29714  lfuhgr  29726  uspgrf1oedg  29754  usgrf1oedg  29788  usgredg3  29797  ushgredgedg  29810  ushgredgedgloop  29812  usgrexmpledg  29843  0grsubgr  29859  uhgrspan1  29884  usgredgffibi  29905  dfnbgr3  29919  nbupgrres  29945  usgrnbcnvfv  29946  edginwlk  30215  wlkiswwlks2lem4  30461  wlkiswwlks2lem5  30462  clwlkclwwlk  30593  ex-rn  31041  bafval  31206  cnnvba  31281  minveco  31486  abrexexd  33105  imadifxp  33195  elrgspn  33807  elrgspnsubrun  33810  lsmsnorb  33946  prsrn  34547  raddcn  34561  pl1cn  34587  esumrnmpt2  34700  sitgclbn  34975  mvtval  36265  elmsubrn  36293  dfon4  36655  ellines  36917  rnmptsn  38258  f1omptsnlem  38259  icoreresf  38275  ptrest  38537  ovoliunnfl  38580  voliunnfl  38582  rngoueqz  38874  rngonegmn1l  38875  rngonegmn1r  38876  rngoneglmul  38877  rngonegrmul  38878  zerdivemp1x  38881  isdrngo2  38892  rngokerinj  38909  iscrngo2  38931  idlnegcl  38956  1idl  38960  0rngo  38961  smprngopr  38986  prnc  39001  isfldidl  39002  isdmn3  39008  rncnvepres  39241  rnqmap  39386  dfsuccl2  39402  imaopab  43285  mzpmfp  43757  dmnonrel  44589  imanonrel  44592  cnvrcl0  44624  ntrrn  45121  modelaxreplem2  45968  modelaxreplem3  45969  rnresun  46194  disjinfi  46206  imassmpt  46273  supxrleubrnmptf  46460  elicores  46544  limsupvaluz  46717  limsupmnflem  46729  limsupvaluz2  46747  limsup10ex  46782  liminf10ex  46783  liminflelimsuplem  46784  ioodvbdlimc1lem1  46940  ioodvbdlimc1  46942  ioodvbdlimc2  46944  fourierdlem42  47158  ioorrnopn  47314  subsaliuncl  47367  sge0sn  47388  sge0split  47418  sge0fodjrnlem  47425  sge0xaddlem2  47443  volicorescl  47562  hoidmvlelem3  47606  vonioolem2  47690  smflimsuplem1  47829  smflimsuplem3  47831  smflimsup  47837  fcoreslem2  48133  dfclnbgr3  48923  isuspgrim0lem  48990  upgrimtrlslem2  49002  usgrexmpl1edg  49121  usgrexmpl2edg  49126