Theorem rneq 5506

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 5451	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5481	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5277	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5277	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2819	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1632  ^◡ccnv 5265  dom cdm 5266  ran crn 5267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-cnv 5274  df-dm 5276  df-rn 5277

This theorem is referenced by:  rneqi  5507  rneqd  5508  feq1  6187  foeq1  6272  fnrnfv  6404  fconst5  6635  frxp  7455  tz7.44-2  7672  tz7.44-3  7673  ixpsnf1o  8114  ordtypecbv  8587  ordtypelem3  8590  dfac8alem  9042  dfac8a  9043  dfac5lem3  9138  dfac9  9150  dfac12lem1  9157  dfac12r  9160  ackbij2  9257  isfin3ds  9343  fin23lem17  9352  fin23lem29  9355  fin23lem30  9356  fin23lem32  9358  fin23lem34  9360  fin23lem35  9361  fin23lem39  9364  fin23lem41  9366  isf33lem  9380  isf34lem6  9394  dcomex  9461  axdc2lem  9462  zorn2lem1  9510  zorn2g  9517  ttukey2g  9530  gruurn  9812  rpnnen1lem6  12012  rpnnen1OLD  12018  relexp0g  13961  relexpsucnnr  13964  dfrtrcl2  14001  mpfrcl  19720  ply1frcl  19885  pnrmopn  21349  isi1f  23640  itg1val  23649  axlowdimlem13  26033  axlowdim1  26038  ausgrusgri  26262  0uhgrsubgr  26370  cusgrsize  26560  ex-rn  27608  gidval  27675  grpoinvfval  27685  grpodivfval  27697  isablo  27709  vciOLD  27725  isvclem  27741  isnvlem  27774  isphg  27981  pj11i  28879  hmopidmch  29321  hmopidmpj  29322  pjss1coi  29331  padct  29806  locfinreflem  30216  locfinref  30217  issibf  30704  sitgfval  30712  mrsubvrs  31726  rdgprc0  32004  rdgprc  32005  dfrdg2  32006  madeval  32241  brrangeg  32349  poimirlem24  33746  volsupnfl  33767  elghomlem1OLD  33997  isdivrngo  34062  iscom2  34107  elrefrels2  34590  elrefrels3  34591  refreleq  34593  elcnvrefrels2  34603  elcnvrefrels3  34604  dnnumch1  38116  aomclem3  38128  aomclem8  38133  rclexi  38424  rtrclex  38426  rtrclexi  38430  cnvrcl0  38434  dfrtrcl5  38438  dfrcl2  38468  csbima12gALTVD  39632  unirnmap  39899  ssmapsn  39907  sge0val  41086  vonvolmbl  41381