Theorem rneqi 5234

Description: Equality inference for range. (Contributed by NM, 4-Mar-2004.)

Hypothesis

Ref	Expression
rneqi.1

Assertion

Ref	Expression
rneqi

Proof of Theorem rneqi

Step	Hyp	Ref	Expression
1		rneqi.1	. 2
2		rneq 5233	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  rancrn 5005

This theorem is referenced by:  rnmpt  5253  resima  5311  resima2  5312  ima0  5357  rnuni  5422  imaundi  5423  imaundir  5424  inimass  5427  dminxp  5452  imainrect  5453  xpima  5454  rnresv  5471  imacnvcnv  5477  rnpropg  5493  imadmres  5504  mptpreima  5505  dmco  5520  resdif  5841  fpr  6079  fliftfuns  6212  rnoprab  6385  rnmpt2  6412  elrnmpt2res  6416  curry1  6892  curry2  6895  fparlem3  6902  fparlem4  6903  qliftfuns  7417  xpassen  7631  sbthlem6  7652  dfsup3OLD  7924  hartogslem1  7988  rankwflemb  8232  fin23lem34  8747  axcc2lem  8837  axdc2lem  8849  fpwwe2lem13  9041  seqval  12118  0rest  14827  imasdsval2  14913  fulloppc  15291  oppchofcl  15529  oyoncl  15539  gsumwspan  16014  pmtrprfvalrn  16513  psgnsn  16545  psgnprfval2  16548  oppglsm  16662  efgredlemg  16760  efgredlemd  16762  dprdvalOLD  17036  pf1rcl  18385  mpfpf1  18387  pf1ind  18391  pjdm  18738  leordtvallem1  19711  leordtvallem2  19712  leordtval  19714  cnconst2  19784  ptcmplem1  20552  tgpconcomp  20611  fmucndlem  20794  fmucnd  20795  ucnextcn  20807  metusttoOLD  21060  metustto  21061  metustexhalfOLD  21066  metustexhalf  21067  metuustOLD  21074  metuust  21075  cfilucfil2OLD  21076  cfilucfil2  21077  metuelOLD  21080  metuel  21081  metutopOLD  21085  psmetutop  21086  restmetu  21090  metucnOLD  21091  metucn  21092  minveclem5  21848  minvec  21851  ovolgelb  21891  ovoliunlem1  21913  itg1addlem4  22106  itg2seq  22149  itg2i1fseq  22162  itg2cnlem1  22168  efifo  22934  logrn  22946  dfrelog  22953  dvrelog  23018  xrlimcnp  23298  usgrares1  24410  cusgrares  24472  ex-rn  25161  rngoueqz  25432  zerdivemp1  25436  rngoridfz  25437  bafval  25497  cnnvba  25584  minveco  25800  abrexexd  27407  imadifxp  27458  prsrn  27897  raddcn  27911  pl1cn  27937  sitgclbn  28285  mvtval  28860  elmsubrn  28888  ghomsn  29028  dfon4  29543  ellines  29802  ptrest  30048  ovoliunnfl  30056  voliunnfl  30058  rngonegmn1l  30352  rngonegmn1r  30353  rngoneglmul  30354  rngonegrmul  30355  zerdivemp1x  30358  isdrngo2  30361  rngokerinj  30378  iscrngo2  30395  idlnegcl  30419  1idl  30423  0rngo  30424  smprngopr  30449  prnc  30464  isfldidl  30465  isdmn3  30471  mzpmfp  30679  mzpmfpOLD  30680  ioodvbdlimc1lem1  31728  ioodvbdlimc1  31730  ioodvbdlimc2  31732  fourierdlem42  31931  usgra2adedglem1  32356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-cnv 5012  df-dm 5014  df-rn 5015