MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rneqi Structured version   Visualization version   GIF version

Theorem rneqi 5259
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
StepHypRef Expression
1 rneqi.1 . 2 𝐴 = 𝐵
2 rneq 5258 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2ax-mp 5 1 ran 𝐴 = ran 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  ran crn 5028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-opab 4638  df-cnv 5035  df-dm 5037  df-rn 5038
This theorem is referenced by:  rnmpt  5278  resima  5337  resima2  5338  resima2OLD  5339  ima0  5386  rnuni  5448  imaundi  5449  imaundir  5450  inimass  5453  dminxp  5478  imainrect  5479  xpima  5480  rnresv  5497  imacnvcnv  5502  rnpropg  5518  imadmres  5529  mptpreima  5530  dmco  5545  resdif  6054  fpr  6303  fliftfuns  6441  rnoprab  6618  rnmpt2  6645  elrnmpt2res  6649  curry1  7133  curry2  7136  fparlem3  7143  fparlem4  7144  qliftfuns  7698  xpassen  7916  sbthlem6  7937  hartogslem1  8307  rankwflemb  8516  fin23lem34  9028  axcc2lem  9118  axdc2lem  9130  fpwwe2lem13  9320  seqval  12631  0rest  15861  imasdsval2  15947  fulloppc  16353  oppchofcl  16671  oyoncl  16681  gsumwspan  17154  pmtrprfvalrn  17679  psgnsn  17711  psgnprfval2  17714  oppglsm  17828  efgredlemg  17926  efgredlemd  17928  pf1rcl  19482  mpfpf1  19484  pf1ind  19488  pjdm  19817  leordtvallem1  20771  leordtvallem2  20772  leordtval  20774  cnconst2  20844  ptcmplem1  21613  tgpconcomp  21673  fmucndlem  21852  fmucnd  21853  ucnextcn  21865  metustto  22115  metustexhalf  22118  metuust  22122  cfilucfil2  22123  metuel  22126  psmetutop  22129  restmetu  22132  metucn  22133  minveclem5  22956  minvec  22959  ovolgelb  22999  ovoliunlem1  23021  itg1addlem4  23216  itg2seq  23259  itg2i1fseq  23272  itg2cnlem1  23278  efifo  24041  logrn  24053  dfrelog  24060  dvrelog  24127  xrlimcnp  24439  usgrares1  25732  cusgrares  25794  ex-rn  26482  bafval  26636  cnnvba  26711  minveco  26917  abrexexd  28524  imadifxp  28589  prsrn  29082  raddcn  29096  pl1cn  29122  esumrnmpt2  29250  sitgclbn  29525  mvtval  30444  elmsubrn  30472  dfon4  30963  ellines  31222  rnmptsn  32141  f1omptsnlem  32142  icoreresf  32159  ptrest  32361  ovoliunnfl  32404  voliunnfl  32406  rngoueqz  32692  rngonegmn1l  32693  rngonegmn1r  32694  rngoneglmul  32695  rngonegrmul  32696  zerdivemp1x  32699  isdrngo2  32710  rngokerinj  32727  iscrngo2  32749  idlnegcl  32774  1idl  32778  0rngo  32779  smprngopr  32804  prnc  32819  isfldidl  32820  isdmn3  32826  mzpmfp  36111  dmnonrel  36698  imanonrel  36701  cnvrcl0  36734  ntrrn  37223  rnresun  38140  disjinfi  38158  rnmpt0  38190  elicores  38390  ioodvbdlimc1lem1  38604  ioodvbdlimc1  38606  ioodvbdlimc2  38608  fourierdlem42  38825  ioorrnopn  38984  subsaliuncl  39035  sge0sn  39055  sge0split  39085  sge0fodjrnlem  39092  sge0xaddlem2  39110  volicorescl  39226  hoidmvlelem3  39270  vonioolem2  39355  uhgrvtxedgiedgb  40350  uspgrf1oedg  40384  usgrf1oedg  40415  usgredg3  40424  ushgredgedga  40437  ushgredgedgaloop  40439  usgrexmpledg  40467  0grsubgr  40483  uhgrspan1  40508  usgredgffibi  40524  dfnbgr3  40543  nbupgrres  40573  usgrnbcnvfv  40574  edginwlk  40820  1wlkiswwlks2lem4  41050  1wlkiswwlks2lem5  41051  clwlkclwwlk  41192
  Copyright terms: Public domain W3C validator