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

Theorem rneqi 5794
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 5793 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2ax-mp 5 1 ran 𝐴 = ran 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  ran crn 5543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4550  df-pr 4552  df-op 4556  df-br 5053  df-opab 5115  df-cnv 5550  df-dm 5552  df-rn 5553
This theorem is referenced by:  rnmpt  5814  resima  5874  resima2  5875  mptima  5928  ima0  5932  rnuni  5994  imaundi  5995  imaundir  5996  inimass  5999  dminxp  6024  imainrect  6025  xpima  6026  rnresv  6045  imacnvcnv  6050  rnpropg  6066  imadmres  6078  mptpreima  6079  dmco  6094  resdif  6623  fpr  6904  rnmptc  6957  fliftfuns  7056  rnoprab  7246  rnmpo  7273  elrnmpores  7277  curry1  7789  curry2  7792  fparlem3  7799  fparlem4  7800  fsplitfpar  7804  qliftfuns  8374  xpassen  8601  sbthlem6  8623  hartogslem1  8997  rankwflemb  9213  fin23lem34  9760  axcc2lem  9850  axdc2lem  9862  fpwwe2lem13  10056  seqval  13380  0rest  16699  imasdsval2  16785  fulloppc  17188  oppchofcl  17506  oyoncl  17516  gsumwspan  18007  pmtrprfvalrn  18612  psgnsn  18644  psgnprfval2  18647  oppglsm  18763  efgredlemg  18864  efgredlemd  18866  fincygsubgodd  19230  pf1rcl  20505  mpfpf1  20507  pf1ind  20511  pjdm  20844  leordtvallem1  21811  leordtvallem2  21812  leordtval  21814  cnconst2  21884  ptcmplem1  22653  tgpconncomp  22714  fmucndlem  22893  fmucnd  22894  ucnextcn  22906  metustto  23156  metustexhalf  23159  metuust  23163  cfilucfil2  23164  metuel  23167  psmetutop  23170  restmetu  23173  metucn  23174  minveclem5  24033  minvec  24036  ovolgelb  24080  ovoliunlem1  24102  itg1addlem4  24299  itg2seq  24342  itg2i1fseq  24355  itg2cnlem1  24361  efifo  25135  logrn  25146  dfrelog  25153  dvrelog  25224  xrlimcnp  25550  iedgedg  26839  edgiedgb  26843  edg0iedg0  26844  uhgrvtxedgiedgb  26925  uspgrf1oedg  26962  usgrf1oedg  26993  usgredg3  27002  ushgredgedg  27015  ushgredgedgloop  27017  usgrexmpledg  27048  0grsubgr  27064  uhgrspan1  27089  usgredgffibi  27110  dfnbgr3  27124  nbupgrres  27150  usgrnbcnvfv  27151  edginwlk  27420  wlkiswwlks2lem4  27654  wlkiswwlks2lem5  27655  clwlkclwwlk  27783  ex-rn  28221  bafval  28383  cnnvba  28458  minveco  28663  abrexexd  30272  imadifxp  30355  lsmsnorb  30971  prsrn  31183  raddcn  31197  pl1cn  31223  esumrnmpt2  31352  sitgclbn  31626  lfuhgr  32389  mvtval  32772  elmsubrn  32800  dfon4  33379  ellines  33638  rnmptsn  34664  f1omptsnlem  34665  icoreresf  34681  ptrest  34966  ovoliunnfl  35009  voliunnfl  35011  rngoueqz  35288  rngonegmn1l  35289  rngonegmn1r  35290  rngoneglmul  35291  rngonegrmul  35292  zerdivemp1x  35295  isdrngo2  35306  rngokerinj  35323  iscrngo2  35345  idlnegcl  35370  1idl  35374  0rngo  35375  smprngopr  35400  prnc  35415  isfldidl  35416  isdmn3  35422  rncnvepres  35631  imaopab  39291  mzpmfp  39541  dmnonrel  40143  imanonrel  40146  cnvrcl0  40178  ntrrn  40681  rnresun  41664  disjinfi  41682  rnmpt0  41711  imassmpt  41765  supxrleubrnmptf  41953  elicores  42033  limsupvaluz  42213  limsupmnflem  42225  limsupvaluz2  42243  limsup10ex  42278  liminf10ex  42279  liminflelimsuplem  42280  ioodvbdlimc1lem1  42436  ioodvbdlimc1  42438  ioodvbdlimc2  42440  fourierdlem42  42654  ioorrnopn  42810  subsaliuncl  42861  sge0sn  42881  sge0split  42911  sge0fodjrnlem  42918  sge0xaddlem2  42936  volicorescl  43055  hoidmvlelem3  43099  vonioolem2  43183  smflimsuplem1  43314  smflimsuplem3  43316  smflimsup  43322
  Copyright terms: Public domain W3C validator