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

Theorem rneqi 5088
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 5087 . 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 4871
This theorem is referenced by:  rnmpt  5108  resima  5170  resima2  5171  ima0  5213  rnuni  5275  imaundi  5276  imaundir  5277  inimass  5280  dminxp  5303  imainrect  5304  xpima  5305  rnresv  5322  imacnvcnv  5326  imadmres  5354  mptpreima  5355  dmco  5370  resdif  5688  fpr  5906  fliftfuns  6028  rnoprab  6148  rnmpt2  6172  curry1  6430  curry2  6433  fparlem3  6440  fparlem4  6441  qliftfuns  6983  xpassen  7194  sbthlem6  7214  dfsup3OLD  7441  hartogslem1  7503  rankwflemb  7711  fin23lem34  8218  axcc2lem  8308  axdc2lem  8320  fpwwe2lem13  8509  seqval  11326  0rest  13649  imasdsval2  13734  fulloppc  14111  oppchofcl  14349  oyoncl  14359  gsumwspan  14783  oppglsm  15268  efgredlemg  15366  efgredlemd  15368  pjdm  16926  leordtvallem1  17266  leordtvallem2  17267  leordtval  17269  cnconst2  17339  ptcmplem1  18075  tgpconcomp  18134  fmucndlem  18313  fmucnd  18314  ucnextcn  18326  metusttoOLD  18579  metustto  18580  metustexhalfOLD  18585  metustexhalf  18586  metuustOLD  18593  metuust  18594  cfilucfil2OLD  18595  cfilucfil2  18596  metuelOLD  18599  metuel  18600  metutopOLD  18604  psmetutop  18605  restmetu  18609  metucnOLD  18610  metucn  18611  minveclem5  19326  minvec  19329  ovolgelb  19368  ovoliunlem1  19390  itg1addlem4  19583  itg2seq  19626  itg2i1fseq  19639  itg2cnlem1  19645  pf1rcl  19961  mpfpf1  19963  pf1ind  19967  efifo  20441  logrn  20448  dfrelog  20455  dvrelog  20520  xrlimcnp  20799  usgrares1  21416  cusgrares  21473  ex-rn  21740  rngoueqz  22010  zerdivemp1  22014  rngoridfz  22015  bafval  22075  cnnvba  22162  minveco  22378  abrexexd  23982  rnpropg  24027  imadifxp  24030  raddcn  24307  sitgclbn  24649  ghomsn  25091  dfon4  25730  ellines  26078  ovoliunnfl  26238  voliunnfl  26240  rngonegmn1l  26556  rngonegmn1r  26557  rngoneglmul  26558  rngonegrmul  26559  zerdivemp1x  26562  isdrngo2  26565  rngokerinj  26582  iscrngo2  26599  idlnegcl  26623  1idl  26627  0rngo  26628  smprngopr  26653  prnc  26668  isfldidl  26669  isdmn3  26675  mzpmfp  26795  usgra2adedglem1  28271
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-cnv 4878  df-dm 4880  df-rn 4881
  Copyright terms: Public domain W3C validator