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

Theorem rneq 5552
Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996.)
Assertion
Ref Expression
rneq (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Proof of Theorem rneq
StepHypRef Expression
1 cnveq 5497 . . 3 (𝐴 = 𝐵𝐴 = 𝐵)
21dmeqd 5527 . 2 (𝐴 = 𝐵 → dom 𝐴 = dom 𝐵)
3 df-rn 5322 . 2 ran 𝐴 = dom 𝐴
4 df-rn 5322 . 2 ran 𝐵 = dom 𝐵
52, 3, 43eqtr4g 2865 1 (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  ccnv 5310  dom cdm 5311  ran crn 5312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845  df-opab 4907  df-cnv 5319  df-dm 5321  df-rn 5322
This theorem is referenced by:  rneqi  5553  rneqd  5554  feq1  6233  foeq1  6323  fnrnfv  6459  fconst5  6692  frxp  7517  tz7.44-2  7735  tz7.44-3  7736  ixpsnf1o  8181  ordtypecbv  8657  ordtypelem3  8660  dfac8alem  9131  dfac8a  9132  dfac5lem3  9227  dfac9  9239  dfac12lem1  9246  dfac12r  9249  ackbij2  9346  isfin3ds  9432  fin23lem17  9441  fin23lem29  9444  fin23lem30  9445  fin23lem32  9447  fin23lem34  9449  fin23lem35  9450  fin23lem39  9453  fin23lem41  9455  isf33lem  9469  isf34lem6  9483  dcomex  9550  axdc2lem  9551  zorn2lem1  9599  zorn2g  9606  ttukey2g  9619  gruurn  9901  rpnnen1lem6  12034  relexp0g  13981  relexpsucnnr  13984  dfrtrcl2  14021  mpfrcl  19722  ply1frcl  19887  pnrmopn  21358  isi1f  23654  itg1val  23663  axlowdimlem13  26047  axlowdim1  26052  ausgrusgri  26277  0uhgrsubgr  26386  cusgrsize  26577  ex-rn  27627  gidval  27694  grpoinvfval  27704  grpodivfval  27716  isablo  27728  vciOLD  27743  isvclem  27759  isnvlem  27792  isphg  27999  pj11i  28897  hmopidmch  29339  hmopidmpj  29340  pjss1coi  29349  padct  29823  locfinreflem  30231  locfinref  30232  issibf  30719  sitgfval  30727  mrsubvrs  31740  rdgprc0  32017  rdgprc  32018  dfrdg2  32019  madeval  32254  brrangeg  32362  poimirlem24  33744  volsupnfl  33765  elghomlem1OLD  33993  isdivrngo  34058  iscom2  34103  elrefrels2  34578  elrefrels3  34579  refreleq  34581  elcnvrefrels2  34591  elcnvrefrels3  34592  dnnumch1  38112  aomclem3  38124  aomclem8  38129  rclexi  38419  rtrclex  38421  rtrclexi  38425  cnvrcl0  38429  dfrtrcl5  38433  dfrcl2  38463  csbima12gALTVD  39624  unirnmap  39884  ssmapsn  39892  sge0val  41059  vonvolmbl  41354
  Copyright terms: Public domain W3C validator