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

Theorem rneqi 5893
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 5892 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2ax-mp 5 1 ran 𝐴 = ran 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  ran crn 5635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-br 5107  df-opab 5169  df-cnv 5642  df-dm 5644  df-rn 5645
This theorem is referenced by:  rnmpt  5911  resima  5972  resima2  5973  mptima  6026  ima0  6030  rnuni  6102  imaundi  6103  imaundir  6104  inimass  6108  dminxp  6133  imainrect  6134  xpima  6135  rnresv  6154  imacnvcnv  6159  rnpropg  6175  imadmres  6187  mptpreima  6191  rnmpt0f  6196  dmco  6207  resdif  6806  fpr  7101  rnmptc  7157  fliftfuns  7260  rnoprab  7461  rnmpo  7490  elrnmpores  7494  curry1  8037  curry2  8040  fparlem3  8047  fparlem4  8048  fsplitfpar  8051  qliftfuns  8746  xpassen  9013  sbthlem6  9035  pwfir  9123  hartogslem1  9483  rnttrcl  9663  rankwflemb  9734  fin23lem34  10287  axcc2lem  10377  axdc2lem  10389  fpwwe2lem12  10583  seqval  13923  0rest  17316  imasdsval2  17403  fulloppc  17814  oppchofcl  18154  oyoncl  18164  gsumwspan  18661  pmtrprfvalrn  19275  psgnsn  19307  psgnprfval2  19310  oppglsm  19429  efgredlemg  19529  efgredlemd  19531  fincygsubgodd  19896  pjdm  21129  pf1rcl  21731  mpfpf1  21733  pf1ind  21737  leordtvallem1  22577  leordtvallem2  22578  leordtval  22580  cnconst2  22650  ptcmplem1  23419  tgpconncomp  23480  fmucndlem  23659  fmucnd  23660  ucnextcn  23672  metustto  23925  metustexhalf  23928  metuust  23932  cfilucfil2  23933  metuel  23936  psmetutop  23939  restmetu  23942  metucn  23943  minveclem5  24813  minvec  24816  ovolgelb  24860  ovoliunlem1  24882  itg1addlem4  25079  itg1addlem4OLD  25080  itg2seq  25123  itg2i1fseq  25136  itg2cnlem1  25142  efifo  25919  logrn  25930  dfrelog  25937  dvrelog  26008  xrlimcnp  26334  iedgedg  28043  edgiedgb  28047  edg0iedg0  28048  uhgrvtxedgiedgb  28129  uspgrf1oedg  28166  usgrf1oedg  28197  usgredg3  28206  ushgredgedg  28219  ushgredgedgloop  28221  usgrexmpledg  28252  0grsubgr  28268  uhgrspan1  28293  usgredgffibi  28314  dfnbgr3  28328  nbupgrres  28354  usgrnbcnvfv  28355  edginwlk  28625  wlkiswwlks2lem4  28859  wlkiswwlks2lem5  28860  clwlkclwwlk  28988  ex-rn  29426  bafval  29588  cnnvba  29663  minveco  29868  abrexexd  31478  imadifxp  31565  lsmsnorb  32220  prsrn  32553  raddcn  32567  pl1cn  32593  esumrnmpt2  32724  sitgclbn  33000  lfuhgr  33768  mvtval  34151  elmsubrn  34179  dfon4  34524  ellines  34783  rnmptsn  35852  f1omptsnlem  35853  icoreresf  35869  ptrest  36123  ovoliunnfl  36166  voliunnfl  36168  rngoueqz  36445  rngonegmn1l  36446  rngonegmn1r  36447  rngoneglmul  36448  rngonegrmul  36449  zerdivemp1x  36452  isdrngo2  36463  rngokerinj  36480  iscrngo2  36502  idlnegcl  36527  1idl  36531  0rngo  36532  smprngopr  36557  prnc  36572  isfldidl  36573  isdmn3  36579  rncnvepres  36810  imaopab  40702  mzpmfp  41113  dmnonrel  41950  imanonrel  41953  cnvrcl0  41985  ntrrn  42482  rnresun  43485  disjinfi  43500  imassmpt  43578  supxrleubrnmptf  43772  elicores  43857  limsupvaluz  44035  limsupmnflem  44047  limsupvaluz2  44065  limsup10ex  44100  liminf10ex  44101  liminflelimsuplem  44102  ioodvbdlimc1lem1  44258  ioodvbdlimc1  44260  ioodvbdlimc2  44262  fourierdlem42  44476  ioorrnopn  44632  subsaliuncl  44685  sge0sn  44706  sge0split  44736  sge0fodjrnlem  44743  sge0xaddlem2  44761  volicorescl  44880  hoidmvlelem3  44924  vonioolem2  45008  smflimsuplem1  45147  smflimsuplem3  45149  smflimsup  45155  fcoreslem2  45384
  Copyright terms: Public domain W3C validator