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

Theorem rneqi 5096
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 5095 . 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 1652   ran crn 4879
This theorem is referenced by:  rnmpt  5116  resima  5178  resima2  5179  ima0  5221  rnuni  5283  imaundi  5284  imaundir  5285  inimass  5288  dminxp  5311  imainrect  5312  xpima  5313  rnresv  5330  imacnvcnv  5334  imadmres  5362  mptpreima  5363  dmco  5378  resdif  5696  fpr  5914  fliftfuns  6036  rnoprab  6156  rnmpt2  6180  curry1  6438  curry2  6441  fparlem3  6448  fparlem4  6449  qliftfuns  6991  xpassen  7202  sbthlem6  7222  dfsup3OLD  7449  hartogslem1  7511  rankwflemb  7719  fin23lem34  8226  axcc2lem  8316  axdc2lem  8328  fpwwe2lem13  8517  seqval  11334  0rest  13657  imasdsval2  13742  fulloppc  14119  oppchofcl  14357  oyoncl  14367  gsumwspan  14791  oppglsm  15276  efgredlemg  15374  efgredlemd  15376  pjdm  16934  leordtvallem1  17274  leordtvallem2  17275  leordtval  17277  cnconst2  17347  ptcmplem1  18083  tgpconcomp  18142  fmucndlem  18321  fmucnd  18322  ucnextcn  18334  metusttoOLD  18587  metustto  18588  metustexhalfOLD  18593  metustexhalf  18594  metuustOLD  18601  metuust  18602  cfilucfil2OLD  18603  cfilucfil2  18604  metuelOLD  18607  metuel  18608  metutopOLD  18612  psmetutop  18613  restmetu  18617  metucnOLD  18618  metucn  18619  minveclem5  19334  minvec  19337  ovolgelb  19376  ovoliunlem1  19398  itg1addlem4  19591  itg2seq  19634  itg2i1fseq  19647  itg2cnlem1  19653  pf1rcl  19969  mpfpf1  19971  pf1ind  19975  efifo  20449  logrn  20456  dfrelog  20463  dvrelog  20528  xrlimcnp  20807  usgrares1  21424  cusgrares  21481  ex-rn  21748  rngoueqz  22018  zerdivemp1  22022  rngoridfz  22023  bafval  22083  cnnvba  22170  minveco  22386  abrexexd  23990  rnpropg  24035  imadifxp  24038  raddcn  24315  sitgclbn  24657  ghomsn  25099  dfon4  25738  ellines  26086  ovoliunnfl  26248  voliunnfl  26250  rngonegmn1l  26565  rngonegmn1r  26566  rngoneglmul  26567  rngonegrmul  26568  zerdivemp1x  26571  isdrngo2  26574  rngokerinj  26591  iscrngo2  26608  idlnegcl  26632  1idl  26636  0rngo  26637  smprngopr  26662  prnc  26677  isfldidl  26678  isdmn3  26684  mzpmfp  26804  usgra2adedglem1  28318
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-br 4213  df-opab 4267  df-cnv 4886  df-dm 4888  df-rn 4889
  Copyright terms: Public domain W3C validator