Theorem rneqi 5962

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

Syntax hints:   = wceq 1537  ran crn 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  rnmpt  5980  resima  6044  resima2  6045  mptima  6101  ima0  6106  rnuni  6180  imaundi  6181  imaundir  6182  inimass  6186  dminxp  6211  imainrect  6212  xpima  6213  rnresv  6232  imacnvcnv  6237  rnpropg  6253  imadmres  6265  mptpreima  6269  rnmpt0f  6274  dmco  6285  resdif  6883  fpr  7188  rnmptc  7244  fliftfuns  7350  rnoprab  7554  rnmpo  7583  elrnmpores  7588  curry1  8145  curry2  8148  fparlem3  8155  fparlem4  8156  fsplitfpar  8159  qliftfuns  8862  xpassen  9132  sbthlem6  9154  pwfir  9383  hartogslem1  9611  rnttrcl  9791  rankwflemb  9862  fin23lem34  10415  axcc2lem  10505  axdc2lem  10517  fpwwe2lem12  10711  seqval  14063  0rest  17489  imasdsval2  17576  fulloppc  17989  oppchofcl  18330  oyoncl  18340  gsumwspan  18881  pmtrprfvalrn  19530  psgnsn  19562  psgnprfval2  19565  oppglsm  19684  efgredlemg  19784  efgredlemd  19786  fincygsubgodd  20156  pjdm  21750  pf1rcl  22374  mpfpf1  22376  pf1ind  22380  leordtvallem1  23239  leordtvallem2  23240  leordtval  23242  cnconst2  23312  ptcmplem1  24081  tgpconncomp  24142  fmucndlem  24321  fmucnd  24322  ucnextcn  24334  metustto  24587  metustexhalf  24590  metuust  24594  cfilucfil2  24595  metuel  24598  psmetutop  24601  restmetu  24604  metucn  24605  minveclem5  25486  minvec  25489  ovolgelb  25534  ovoliunlem1  25556  itg1addlem4  25753  itg1addlem4OLD  25754  itg2seq  25797  itg2i1fseq  25810  itg2cnlem1  25816  efifo  26607  logrn  26618  dfrelog  26625  dvrelog  26697  xrlimcnp  27029  iedgedg  29085  edgiedgb  29089  edg0iedg0  29090  uhgrvtxedgiedgb  29171  uspgrf1oedg  29208  usgrf1oedg  29242  usgredg3  29251  ushgredgedg  29264  ushgredgedgloop  29266  usgrexmpledg  29297  0grsubgr  29313  uhgrspan1  29338  usgredgffibi  29359  dfnbgr3  29373  nbupgrres  29399  usgrnbcnvfv  29400  edginwlk  29671  wlkiswwlks2lem4  29905  wlkiswwlks2lem5  29906  clwlkclwwlk  30034  ex-rn  30472  bafval  30636  cnnvba  30711  minveco  30916  abrexexd  32537  imadifxp  32623  lsmsnorb  33384  prsrn  33861  raddcn  33875  pl1cn  33901  esumrnmpt2  34032  sitgclbn  34308  lfuhgr  35085  mvtval  35468  elmsubrn  35496  dfon4  35857  ellines  36116  rnmptsn  37301  f1omptsnlem  37302  icoreresf  37318  ptrest  37579  ovoliunnfl  37622  voliunnfl  37624  rngoueqz  37900  rngonegmn1l  37901  rngonegmn1r  37902  rngoneglmul  37903  rngonegrmul  37904  zerdivemp1x  37907  isdrngo2  37918  rngokerinj  37935  iscrngo2  37957  idlnegcl  37982  1idl  37986  0rngo  37987  smprngopr  38012  prnc  38027  isfldidl  38028  isdmn3  38034  rncnvepres  38259  imaopab  42224  mzpmfp  42703  dmnonrel  43552  imanonrel  43555  cnvrcl0  43587  ntrrn  44084  rnresun  45087  disjinfi  45099  imassmpt  45172  supxrleubrnmptf  45366  elicores  45451  limsupvaluz  45629  limsupmnflem  45641  limsupvaluz2  45659  limsup10ex  45694  liminf10ex  45695  liminflelimsuplem  45696  ioodvbdlimc1lem1  45852  ioodvbdlimc1  45854  ioodvbdlimc2  45856  fourierdlem42  46070  ioorrnopn  46226  subsaliuncl  46279  sge0sn  46300  sge0split  46330  sge0fodjrnlem  46337  sge0xaddlem2  46355  volicorescl  46474  hoidmvlelem3  46518  vonioolem2  46602  smflimsuplem1  46741  smflimsuplem3  46743  smflimsup  46749  fcoreslem2  46979  dfclnbgr3  47699  isuspgrim0lem  47755  uspgrimprop  47757  usgrexmpl1edg  47839  usgrexmpl2edg  47844