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

Theorem rneqi 5384
Description: Equality inference for range. (Contributed by NM, 4-Mar-2004.)
Hypothesis
Ref Expression
rneqi.1 𝐴 = 𝐵
Assertion
Ref Expression
rneqi ran 𝐴 = ran 𝐵

Proof of Theorem rneqi
StepHypRef Expression
1 rneqi.1 . 2 𝐴 = 𝐵
2 rneq 5383 . 2 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
31, 2ax-mp 5 1 ran 𝐴 = ran 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  ran crn 5144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-cnv 5151  df-dm 5153  df-rn 5154
This theorem is referenced by:  rnmpt  5403  resima  5466  resima2  5467  resima2OLD  5468  ima0  5516  rnuni  5579  imaundi  5580  imaundir  5581  inimass  5584  dminxp  5609  imainrect  5610  xpima  5611  rnresv  5629  imacnvcnv  5634  rnpropg  5651  imadmres  5665  mptpreima  5666  dmco  5681  resdif  6195  fpr  6461  fliftfuns  6604  rnoprab  6785  rnmpt2  6812  elrnmpt2res  6816  curry1  7314  curry2  7317  fparlem3  7324  fparlem4  7325  qliftfuns  7877  xpassen  8095  sbthlem6  8116  hartogslem1  8488  rankwflemb  8694  fin23lem34  9206  axcc2lem  9296  axdc2lem  9308  fpwwe2lem13  9502  seqval  12852  0rest  16137  imasdsval2  16223  fulloppc  16629  oppchofcl  16947  oyoncl  16957  gsumwspan  17430  pmtrprfvalrn  17954  psgnsn  17986  psgnprfval2  17989  oppglsm  18103  efgredlemg  18201  efgredlemd  18203  pf1rcl  19761  mpfpf1  19763  pf1ind  19767  pjdm  20099  leordtvallem1  21062  leordtvallem2  21063  leordtval  21065  cnconst2  21135  ptcmplem1  21903  tgpconncomp  21963  fmucndlem  22142  fmucnd  22143  ucnextcn  22155  metustto  22405  metustexhalf  22408  metuust  22412  cfilucfil2  22413  metuel  22416  psmetutop  22419  restmetu  22422  metucn  22423  minveclem5  23250  minvec  23253  ovolgelb  23294  ovoliunlem1  23316  itg1addlem4  23511  itg2seq  23554  itg2i1fseq  23567  itg2cnlem1  23573  efifo  24338  logrn  24350  dfrelog  24357  dvrelog  24428  xrlimcnp  24740  iedgedg  25988  edgiedgb  25992  edg0iedg0  25994  uhgrvtxedgiedgb  26076  uspgrf1oedg  26113  usgrf1oedg  26144  usgredg3  26153  ushgredgedg  26166  ushgredgedgloop  26168  usgrexmpledg  26199  0grsubgr  26215  uhgrspan1  26240  usgredgffibi  26261  dfnbgr3  26276  nbupgrres  26310  usgrnbcnvfv  26311  edginwlk  26586  edginwlkOLD  26587  wlkiswwlks2lem4  26826  wlkiswwlks2lem5  26827  clwlkclwwlk  26968  ex-rn  27427  bafval  27587  cnnvba  27662  minveco  27868  abrexexd  29473  imadifxp  29540  prsrn  30089  raddcn  30103  pl1cn  30129  esumrnmpt2  30258  sitgclbn  30533  mvtval  31523  elmsubrn  31551  dfon4  32125  ellines  32384  rnmptsn  33312  f1omptsnlem  33313  icoreresf  33330  ptrest  33538  ovoliunnfl  33581  voliunnfl  33583  rngoueqz  33869  rngonegmn1l  33870  rngonegmn1r  33871  rngoneglmul  33872  rngonegrmul  33873  zerdivemp1x  33876  isdrngo2  33887  rngokerinj  33904  iscrngo2  33926  idlnegcl  33951  1idl  33955  0rngo  33956  smprngopr  33981  prnc  33996  isfldidl  33997  isdmn3  34003  rncnvepres  34214  mzpmfp  37627  dmnonrel  38213  imanonrel  38216  cnvrcl0  38249  ntrrn  38737  rnresun  39676  disjinfi  39694  rnmpt0  39726  mptima  39751  imassmpt  39795  supxrleubrnmptf  39993  elicores  40078  limsupvaluz  40258  limsupmnflem  40270  limsupvaluz2  40288  limsup10ex  40323  liminf10ex  40324  liminflelimsuplem  40325  ioodvbdlimc1lem1  40464  ioodvbdlimc1  40466  ioodvbdlimc2  40468  fourierdlem42  40684  ioorrnopn  40843  subsaliuncl  40894  sge0sn  40914  sge0split  40944  sge0fodjrnlem  40951  sge0xaddlem2  40969  volicorescl  41088  hoidmvlelem3  41132  vonioolem2  41216  smflimsuplem1  41347  smflimsuplem3  41349  smflimsup  41355
  Copyright terms: Public domain W3C validator