Theorem rneq 5383

Description: Equality theorem for range. (Contributed by NM, 29-Dec-1996.)

Assertion

Ref	Expression
rneq	⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Proof of Theorem rneq

Step	Hyp	Ref	Expression
1		cnveq 5328	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5358	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5154	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5154	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2710	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1523  ^◡ccnv 5142  dom cdm 5143  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:  rneqi  5384  rneqd  5385  feq1  6064  foeq1  6149  fnrnfv  6281  fconst5  6512  frxp  7332  tz7.44-2  7548  tz7.44-3  7549  ixpsnf1o  7990  ordtypecbv  8463  ordtypelem3  8466  dfac8alem  8890  dfac8a  8891  dfac5lem3  8986  dfac9  8996  dfac12lem1  9003  dfac12r  9006  ackbij2  9103  isfin3ds  9189  fin23lem17  9198  fin23lem29  9201  fin23lem30  9202  fin23lem32  9204  fin23lem34  9206  fin23lem35  9207  fin23lem39  9210  fin23lem41  9212  isf33lem  9226  isf34lem6  9240  dcomex  9307  axdc2lem  9308  zorn2lem1  9356  zorn2g  9363  ttukey2g  9376  gruurn  9658  rpnnen1lem6  11857  rpnnen1OLD  11863  relexp0g  13806  relexpsucnnr  13809  dfrtrcl2  13846  mpfrcl  19566  ply1frcl  19731  pnrmopn  21195  isi1f  23486  itg1val  23495  axlowdimlem13  25879  axlowdim1  25884  ausgrusgri  26108  0uhgrsubgr  26216  cusgrsize  26406  ex-rn  27427  gidval  27494  grpoinvfval  27504  grpodivfval  27516  isablo  27528  vciOLD  27544  isvclem  27560  isnvlem  27593  isphg  27800  pj11i  28698  hmopidmch  29140  hmopidmpj  29141  pjss1coi  29150  padct  29625  locfinreflem  30035  locfinref  30036  issibf  30523  sitgfval  30531  mrsubvrs  31545  rdgprc0  31823  rdgprc  31824  dfrdg2  31825  madeval  32060  brrangeg  32168  poimirlem24  33563  volsupnfl  33584  elghomlem1OLD  33814  isdivrngo  33879  iscom2  33924  elrefrels2  34407  elrefrels3  34408  refreleq  34410  elcnvrefrels2  34420  elcnvrefrels3  34421  dnnumch1  37931  aomclem3  37943  aomclem8  37948  rclexi  38239  rtrclex  38241  rtrclexi  38245  cnvrcl0  38249  dfrtrcl5  38253  dfrcl2  38283  csbima12gALTVD  39447  unirnmap  39714  ssmapsn  39722  sge0val  40901  vonvolmbl  41196