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

Theorem rneqi 5055
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 5054 . 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 4838
This theorem is referenced by:  rnmpt  5075  resima  5137  resima2  5138  ima0  5180  rnuni  5242  imaundi  5243  imaundir  5244  inimass  5247  dminxp  5270  imainrect  5271  xpima  5272  rnresv  5289  imacnvcnv  5293  imadmres  5321  mptpreima  5322  dmco  5337  resdif  5655  fpr  5873  fliftfuns  5995  rnoprab  6115  rnmpt2  6139  curry1  6397  curry2  6400  fparlem3  6407  fparlem4  6408  qliftfuns  6950  xpassen  7161  sbthlem6  7181  dfsup3OLD  7407  hartogslem1  7467  rankwflemb  7675  fin23lem34  8182  axcc2lem  8272  axdc2lem  8284  fpwwe2lem13  8473  seqval  11289  0rest  13612  imasdsval2  13697  fulloppc  14074  oppchofcl  14312  oyoncl  14322  gsumwspan  14746  oppglsm  15231  efgredlemg  15329  efgredlemd  15331  pjdm  16889  leordtvallem1  17228  leordtvallem2  17229  leordtval  17231  cnconst2  17301  ptcmplem1  18036  tgpconcomp  18095  fmucndlem  18274  fmucnd  18275  ucnextcn  18287  metusttoOLD  18540  metustto  18541  metustexhalfOLD  18546  metustexhalf  18547  metuustOLD  18554  metuust  18555  cfilucfil2OLD  18556  cfilucfil2  18557  metuelOLD  18560  metuel  18561  metutopOLD  18565  psmetutop  18566  restmetu  18570  metucnOLD  18571  metucn  18572  minveclem5  19287  minvec  19290  ovolgelb  19329  ovoliunlem1  19351  itg1addlem4  19544  itg2seq  19587  itg2i1fseq  19600  itg2cnlem1  19606  pf1rcl  19922  mpfpf1  19924  pf1ind  19928  efifo  20402  logrn  20409  dfrelog  20416  dvrelog  20481  xrlimcnp  20760  usgrares1  21377  cusgrares  21434  ex-rn  21701  rngoueqz  21971  zerdivemp1  21975  rngoridfz  21976  bafval  22036  cnnvba  22123  minveco  22339  abrexexd  23943  rnpropg  23988  imadifxp  23991  raddcn  24268  sitgclbn  24610  ghomsn  25052  dfon4  25647  ellines  25990  ovoliunnfl  26147  voliunnfl  26149  rngonegmn1l  26455  rngonegmn1r  26456  rngoneglmul  26457  rngonegrmul  26458  zerdivemp1x  26461  isdrngo2  26464  rngokerinj  26481  iscrngo2  26498  idlnegcl  26522  1idl  26526  0rngo  26527  smprngopr  26552  prnc  26567  isfldidl  26568  isdmn3  26574  mzpmfp  26694  usgra2adedglem1  28048
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-cnv 4845  df-dm 4847  df-rn 4848
  Copyright terms: Public domain W3C validator