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

Theorem rneqi 5029
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 5028 . 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 1649   ran crn 4812
This theorem is referenced by:  rnmpt  5049  resima  5111  resima2  5112  ima0  5154  rnuni  5216  imaundi  5217  imaundir  5218  inimass  5221  dminxp  5244  imainrect  5245  xpima  5246  rnresv  5263  imacnvcnv  5267  imadmres  5295  mptpreima  5296  dmco  5311  resdif  5629  fpr  5846  fliftfuns  5968  rnoprab  6088  rnmpt2  6112  curry1  6370  curry2  6373  fparlem3  6380  fparlem4  6381  qliftfuns  6920  xpassen  7131  sbthlem6  7151  dfsup3OLD  7377  hartogslem1  7437  rankwflemb  7645  fin23lem34  8152  axcc2lem  8242  axdc2lem  8254  fpwwe2lem13  8443  seqval  11254  0rest  13577  imasdsval2  13662  fulloppc  14039  oppchofcl  14277  oyoncl  14287  gsumwspan  14711  oppglsm  15196  efgredlemg  15294  efgredlemd  15296  pjdm  16850  leordtvallem1  17189  leordtvallem2  17190  leordtval  17192  cnconst2  17262  ptcmplem1  17997  tgpconcomp  18056  fmucndlem  18235  fmucnd  18236  ucnextcn  18248  metustto  18466  metustexhalf  18469  metuust  18473  cfilucfil2  18474  metuel  18477  metutop  18480  restmetu  18482  metucn  18483  minveclem5  19194  minvec  19197  ovolgelb  19236  ovoliunlem1  19258  itg1addlem4  19451  itg2seq  19494  itg2i1fseq  19507  itg2cnlem1  19513  pf1rcl  19829  mpfpf1  19831  pf1ind  19835  efifo  20309  logrn  20316  dfrelog  20323  dvrelog  20388  xrlimcnp  20667  usgrares1  21283  cusgrares  21340  ex-rn  21589  rngoueqz  21859  zerdivemp1  21863  rngoridfz  21864  bafval  21924  cnnvba  22011  minveco  22227  abrexexd  23827  rnpropg  23871  imadifxp  23874  raddcn  24112  ghomsn  24871  dfon4  25450  ellines  25793  ovoliunnfl  25946  voliunnfl  25948  rngonegmn1l  26249  rngonegmn1r  26250  rngoneglmul  26251  rngonegrmul  26252  zerdivemp1x  26255  isdrngo2  26258  rngokerinj  26275  iscrngo2  26292  idlnegcl  26316  1idl  26320  0rngo  26321  smprngopr  26346  prnc  26361  isfldidl  26362  isdmn3  26368  mzpmfp  26488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-br 4147  df-opab 4201  df-cnv 4819  df-dm 4821  df-rn 4822
  Copyright terms: Public domain W3C validator