Theorem rneq 5806

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 5744	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5774	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5566	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5566	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2881	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

Syntax hints:   → wi 4   = wceq 1537  ^◡ccnv 5554  dom cdm 5555  ran crn 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-cnv 5563  df-dm 5565  df-rn 5566

This theorem is referenced by:  rneqi  5807  rneqd  5808  feq1  6495  foeq1  6586  fnrnfv  6725  fconst5  6968  frxp  7820  tz7.44-2  8043  tz7.44-3  8044  ixpsnf1o  8502  ordtypecbv  8981  ordtypelem3  8984  dfac8alem  9455  dfac8a  9456  dfac5lem3  9551  dfac9  9562  dfac12lem1  9569  dfac12r  9572  ackbij2  9665  isfin3ds  9751  fin23lem17  9760  fin23lem29  9763  fin23lem30  9764  fin23lem32  9766  fin23lem34  9768  fin23lem35  9769  fin23lem39  9772  fin23lem41  9774  isf33lem  9788  isf34lem6  9802  dcomex  9869  axdc2lem  9870  zorn2lem1  9918  zorn2g  9925  ttukey2g  9938  gruurn  10220  rpnnen1lem6  12382  relexp0g  14381  relexpsucnnr  14384  dfrtrcl2  14421  mpfrcl  20298  selvval  20331  ply1frcl  20481  pnrmopn  21951  isi1f  24275  itg1val  24284  axlowdimlem13  26740  axlowdim1  26745  ausgrusgri  26953  0uhgrsubgr  27061  cusgrsize  27236  ex-rn  28219  gidval  28289  grpoinvfval  28299  grpodivfval  28311  isablo  28323  vciOLD  28338  isvclem  28354  isnvlem  28387  isphg  28594  pj11i  29488  hmopidmch  29930  hmopidmpj  29931  pjss1coi  29940  padct  30455  tocyc01  30760  tocyccntz  30786  locfinreflem  31104  locfinref  31105  issibf  31591  sitgfval  31599  mrsubvrs  32769  rdgprc0  33038  rdgprc  33039  dfrdg2  33040  madeval  33289  brrangeg  33397  poimirlem24  34931  volsupnfl  34952  elghomlem1OLD  35178  isdivrngo  35243  iscom2  35288  elrefrels2  35772  elrefrels3  35773  refreleq  35775  elcnvrefrels2  35785  elcnvrefrels3  35786  dnnumch1  39664  aomclem3  39676  aomclem8  39681  rclexi  39995  rtrclex  39997  rtrclexi  40001  cnvrcl0  40005  dfrtrcl5  40009  dfrcl2  40039  csbima12gALTVD  41251  unirnmap  41491  ssmapsn  41499  sge0val  42668  vonvolmbl  42963