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

Theorem rneqi 4921
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 4920 . 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 1632   ran crn 4706
This theorem is referenced by:  rnmpt  4941  resima  5003  resima2  5004  ima0  5046  rnuni  5108  imaundi  5109  imaundir  5110  dminxp  5134  imainrect  5135  rnresv  5149  imacnvcnv  5153  imadmres  5181  mptpreima  5182  dmco  5197  resdif  5510  fpr  5720  fliftfuns  5829  rnoprab  5946  rnmpt2  5970  curry1  6226  curry2  6229  fparlem3  6236  fparlem4  6237  qliftfuns  6761  xpassen  6972  sbthlem6  6992  dfsup3OLD  7213  hartogslem1  7273  rankwflemb  7481  fin23lem34  7988  axcc2lem  8078  axdc2lem  8090  fpwwe2lem13  8280  seqval  11073  0rest  13350  imasdsval2  13435  fulloppc  13812  oppchofcl  14050  oyoncl  14060  gsumwspan  14484  oppglsm  14969  efgredlemg  15067  efgredlemd  15069  pjdm  16623  leordtvallem1  16956  leordtvallem2  16957  leordtval  16959  cnconst2  17027  ptcmplem1  17762  tgpconcomp  17811  minveclem5  18813  minvec  18816  ovolgelb  18855  ovoliunlem1  18877  itg1addlem4  19070  itg2seq  19113  itg2i1fseq  19126  itg2cnlem1  19132  pf1rcl  19448  mpfpf1  19450  pf1ind  19454  efifo  19925  logrn  19932  dfrelog  19939  dvrelog  20000  xrlimcnp  20279  ex-rn  20843  rngoueqz  21113  bafval  21176  cnnvba  21263  minveco  21479  rnpropg  23205  abrexexd  23207  xpima  23217  raddcn  23317  ghomsn  24010  dfon4  24504  ellines  24847  ovoliunnfl  25001  domrancur1b  25303  domrancur1c  25305  rninc  25384  ranncnt  25386  trooo  25497  zerdivemp1  25539  rngoridfz  25540  vecval3b  25555  vecax4  25559  vecax5  25560  invaddvec  25570  prodvs  25571  dblsubvec  25577  mvecrtol2  25580  mulveczer  25582  mulinvsca  25583  muldisc  25584  vecax5c  25586  svli2  25587  tcnvec  25793  rdmob  25851  dmrngcmp  25854  prismorcsetlemc  26020  rngonegmn1l  26683  rngonegmn1r  26684  rngoneglmul  26685  rngonegrmul  26686  zerdivemp1x  26689  isdrngo2  26692  rngokerinj  26709  iscrngo2  26726  idlnegcl  26750  1idl  26754  0rngo  26755  smprngopr  26780  prnc  26795  isfldidl  26796  isdmn3  26802  mzpmfp  26928
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040  df-opab 4094  df-cnv 4713  df-dm 4715  df-rn 4716
  Copyright terms: Public domain W3C validator