Theorem rneqi 5929

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is used by:  rnmpt  5949  resima  6016  resima2  6017  mptima  6076  ima0  6081  rnuni  6148  imaundi  6149  imaundir  6150  inimass  6154  dminxp  6180  imainrect  6181  xpima  6182  rnresv  6202  imadifssran  6204  imacnvcnv  6209  rnpropg  6225  imadmres  6237  mptpreima  6241  rnmpt0f  6246  dmco  6258  resdif  6846  fpr  7157  rnmptc  7212  fliftfuns  7321  rnoprab  7524  rnmpo  7552  elrnmpores  7557  curry1  8105  curry2  8108  fparlem3  8115  fparlem4  8116  fsplitfpar  8119  qliftfuns  8808  xpassen  9066  sbthlem6  9087  pwfir  9283  hartogslem1  9511  rnttrcl  9698  rankwflemb  9772  fin23lem34  10345  axcc2lem  10435  axdc2lem  10447  fpwwe2lem12  10644  seqval  14068  0rest  17506  imasdsval2  17594  fulloppc  18005  oppchofcl  18340  oyoncl  18350  gsumwspan  18944  pmtrprfvalrn  19604  psgnsn  19636  psgnprfval2  19639  oppglsm  19758  efgredlemg  19858  efgredlemd  19860  fincygsubgodd  20230  pjdm  21909  pf1rcl  22561  mpfpf1  22563  pf1ind  22567  leordtvallem1  23419  leordtvallem2  23420  leordtval  23422  cnconst2  23492  ptcmplem1  24262  tgpconncomp  24323  fmucndlem  24500  fmucnd  24501  ucnextcn  24513  metustto  24763  metustexhalf  24766  metuust  24770  cfilucfil2  24771  metuel  24774  psmetutop  24777  restmetu  24780  metucn  24781  minveclem5  25645  minvec  25648  ovolgelb  25692  ovoliunlem1  25714  itg1addlem4  25911  itg2seq  25954  itg2i1fseq  25967  itg2cnlem1  25973  efifo  26765  logrn  26776  dfrelog  26783  dvrelog  26855  xrlimcnp  27186  iedgedg  29457  edgiedgb  29461  edg0iedg0  29462  uhgrvtxedgiedgb  29543  lfuhgr  29555  uspgrf1oedg  29583  usgrf1oedg  29617  usgredg3  29626  ushgredgedg  29639  ushgredgedgloop  29641  usgrexmpledg  29672  0grsubgr  29688  uhgrspan1  29713  usgredgffibi  29734  dfnbgr3  29748  nbupgrres  29774  usgrnbcnvfv  29775  edginwlk  30044  wlkiswwlks2lem4  30290  wlkiswwlks2lem5  30291  clwlkclwwlk  30422  ex-rn  30864  bafval  31029  cnnvba  31104  minveco  31309  abrexexd  32928  imadifxp  33019  elrgspn  33632  elrgspnsubrun  33635  lsmsnorb  33770  prsrn  34371  raddcn  34385  pl1cn  34411  esumrnmpt2  34524  sitgclbn  34800  mvtval  36031  elmsubrn  36059  dfon4  36422  ellines  36683  rnmptsn  38040  f1omptsnlem  38041  icoreresf  38057  ptrest  38329  ovoliunnfl  38372  voliunnfl  38374  rngoueqz  38651  rngonegmn1l  38652  rngonegmn1r  38653  rngoneglmul  38654  rngonegrmul  38655  zerdivemp1x  38658  isdrngo2  38669  rngokerinj  38686  iscrngo2  38708  idlnegcl  38733  1idl  38737  0rngo  38738  smprngopr  38763  prnc  38778  isfldidl  38779  isdmn3  38785  rncnvepres  39018  rnqmap  39163  dfsuccl2  39179  imaopab  43062  mzpmfp  43538  dmnonrel  44376  imanonrel  44379  cnvrcl0  44411  ntrrn  44908  modelaxreplem2  45748  modelaxreplem3  45749  rnresun  45958  disjinfi  45970  imassmpt  46037  supxrleubrnmptf  46225  elicores  46309  limsupvaluz  46482  limsupmnflem  46494  limsupvaluz2  46512  limsup10ex  46547  liminf10ex  46548  liminflelimsuplem  46549  ioodvbdlimc1lem1  46705  ioodvbdlimc1  46707  ioodvbdlimc2  46709  fourierdlem42  46923  ioorrnopn  47079  subsaliuncl  47132  sge0sn  47153  sge0split  47183  sge0fodjrnlem  47190  sge0xaddlem2  47208  volicorescl  47327  hoidmvlelem3  47371  vonioolem2  47455  smflimsuplem1  47594  smflimsuplem3  47596  smflimsup  47602  fcoreslem2  47861  dfclnbgr3  48651  isuspgrim0lem  48718  upgrimtrlslem2  48730  usgrexmpl1edg  48849  usgrexmpl2edg  48854