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

Theorem rneqi 4905
Description: Equality inference for range. (Contributed by NM, 4-Mar-2004.)
Hypothesis
Ref Expression
rneqi.1  |-  A  =  B
Assertion
Ref Expression
rneqi  |-  ran  A  =  ran  B

Proof of Theorem rneqi
StepHypRef Expression
1 rneqi.1 . 2  |-  A  =  B
2 rneq 4904 . 2  |-  ( A  =  B  ->  ran  A  =  ran  B )
31, 2ax-mp 8 1  |-  ran  A  =  ran  B
Colors of variables: wff set class
Syntax hints:    = wceq 1623   ran crn 4690
This theorem is referenced by:  rnmpt  4925  resima  4987  resima2  4988  ima0  5030  rnuni  5092  imaundi  5093  imaundir  5094  dminxp  5118  imainrect  5119  rnresv  5133  imacnvcnv  5137  imadmres  5165  mptpreima  5166  dmco  5181  resdif  5494  fpr  5704  fliftfuns  5813  rnoprab  5930  rnmpt2  5954  curry1  6210  curry2  6213  fparlem3  6220  fparlem4  6221  qliftfuns  6745  xpassen  6956  sbthlem6  6976  dfsup3OLD  7197  hartogslem1  7257  rankwflemb  7465  fin23lem34  7972  axcc2lem  8062  axdc2lem  8074  fpwwe2lem13  8264  seqval  11057  0rest  13334  imasdsval2  13419  fulloppc  13796  oppchofcl  14034  oyoncl  14044  gsumwspan  14468  oppglsm  14953  efgredlemg  15051  efgredlemd  15053  pjdm  16607  leordtvallem1  16940  leordtvallem2  16941  leordtval  16943  cnconst2  17011  ptcmplem1  17746  tgpconcomp  17795  minveclem5  18797  minvec  18800  ovolgelb  18839  ovoliunlem1  18861  itg1addlem4  19054  itg2seq  19097  itg2i1fseq  19110  itg2cnlem1  19116  pf1rcl  19432  mpfpf1  19434  pf1ind  19438  efifo  19909  logrn  19916  dfrelog  19923  dvrelog  19984  xrlimcnp  20263  ex-rn  20827  rngoueqz  21097  bafval  21160  cnnvba  21247  minveco  21463  rnpropg  23189  abrexexd  23192  xpima  23202  raddcn  23302  ghomsn  23995  dfon4  24433  ellines  24775  domrancur1b  25200  domrancur1c  25202  rninc  25281  ranncnt  25283  trooo  25394  zerdivemp1  25436  rngoridfz  25437  vecval3b  25452  vecax4  25456  vecax5  25457  invaddvec  25467  prodvs  25468  dblsubvec  25474  mvecrtol2  25477  mulveczer  25479  mulinvsca  25480  muldisc  25481  vecax5c  25483  svli2  25484  tcnvec  25690  rdmob  25748  dmrngcmp  25751  prismorcsetlemc  25917  rngonegmn1l  26580  rngonegmn1r  26581  rngoneglmul  26582  rngonegrmul  26583  zerdivemp1x  26586  isdrngo2  26589  rngokerinj  26606  iscrngo2  26623  idlnegcl  26647  1idl  26651  0rngo  26652  smprngopr  26677  prnc  26692  isfldidl  26693  isdmn3  26699  mzpmfp  26825
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-cnv 4697  df-dm 4699  df-rn 4700
  Copyright terms: Public domain W3C validator