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

Theorem rneqi 4907
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 4906 . 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 1625   ran crn 4692
This theorem is referenced by:  rnmpt  4927  resima  4989  resima2  4990  ima0  5032  rnuni  5094  imaundi  5095  imaundir  5096  dminxp  5120  imainrect  5121  rnresv  5135  imacnvcnv  5139  imadmres  5167  mptpreima  5168  dmco  5183  resdif  5496  fpr  5706  fliftfuns  5815  rnoprab  5932  rnmpt2  5956  curry1  6212  curry2  6215  fparlem3  6222  fparlem4  6223  qliftfuns  6747  xpassen  6958  sbthlem6  6978  dfsup3OLD  7199  hartogslem1  7259  rankwflemb  7467  fin23lem34  7974  axcc2lem  8064  axdc2lem  8076  fpwwe2lem13  8266  seqval  11059  0rest  13336  imasdsval2  13421  fulloppc  13798  oppchofcl  14036  oyoncl  14046  gsumwspan  14470  oppglsm  14955  efgredlemg  15053  efgredlemd  15055  pjdm  16609  leordtvallem1  16942  leordtvallem2  16943  leordtval  16945  cnconst2  17013  ptcmplem1  17748  tgpconcomp  17797  minveclem5  18799  minvec  18802  ovolgelb  18841  ovoliunlem1  18863  itg1addlem4  19056  itg2seq  19099  itg2i1fseq  19112  itg2cnlem1  19118  pf1rcl  19434  mpfpf1  19436  pf1ind  19440  efifo  19911  logrn  19918  dfrelog  19925  dvrelog  19986  xrlimcnp  20265  ex-rn  20829  rngoueqz  21099  bafval  21162  cnnvba  21249  minveco  21465  rnpropg  23191  abrexexd  23194  xpima  23204  raddcn  23304  ghomsn  23997  dfon4  24435  ellines  24777  domrancur1b  25211  domrancur1c  25213  rninc  25292  ranncnt  25294  trooo  25405  zerdivemp1  25447  rngoridfz  25448  vecval3b  25463  vecax4  25467  vecax5  25468  invaddvec  25478  prodvs  25479  dblsubvec  25485  mvecrtol2  25488  mulveczer  25490  mulinvsca  25491  muldisc  25492  vecax5c  25494  svli2  25495  tcnvec  25701  rdmob  25759  dmrngcmp  25762  prismorcsetlemc  25928  rngonegmn1l  26591  rngonegmn1r  26592  rngoneglmul  26593  rngonegrmul  26594  zerdivemp1x  26597  isdrngo2  26600  rngokerinj  26617  iscrngo2  26634  idlnegcl  26658  1idl  26662  0rngo  26663  smprngopr  26688  prnc  26703  isfldidl  26704  isdmn3  26710  mzpmfp  26836
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-opab 4080  df-cnv 4699  df-dm 4701  df-rn 4702
  Copyright terms: Public domain W3C validator