Theorem rneq 5917

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 5850	. . 3 ⊢ (𝐴 = 𝐵 → ◡𝐴 = ◡𝐵)
2	1	dmeqd 5886	. 2 ⊢ (𝐴 = 𝐵 → dom ◡𝐴 = dom ◡𝐵)
3		df-rn 5661	. 2 ⊢ ran 𝐴 = dom ◡𝐴
4		df-rn 5661	. 2 ⊢ ran 𝐵 = dom ◡𝐵
5	2, 3, 4	3eqtr4g 2820	1 ⊢ (𝐴 = 𝐵 → ran 𝐴 = ran 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ^◡ccnv 5649  dom cdm 5650  ran crn 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5658  df-dm 5660  df-rn 5661

This theorem is used by:  rneqi  5918  rneqd  5919  feq1  6687  foeq1  6792  fnrnfv  6944  fconst5  7212  frxp  8140  tz7.44-2  8418  tz7.44-3  8419  ixpsnf1o  8969  ordtypecbv  9514  ordtypelem3  9517  dfac8alem  10111  dfac8a  10112  dfac5lem3  10207  dfac9  10218  dfac12lem1  10225  dfac12r  10228  ackbij2  10323  isfin3ds  10410  fin23lem17  10419  fin23lem29  10422  fin23lem30  10423  fin23lem32  10425  fin23lem34  10427  fin23lem35  10428  fin23lem39  10431  fin23lem41  10433  isf33lem  10447  isf34lem6  10461  dcomex  10528  axdc2lem  10529  zorn2lem1  10577  zorn2g  10584  ttukey2g  10597  gruurn  10886  rpnnen1lem6  13113  relexp0g  15180  relexpsucnnr  15183  dfrtrcl2  15220  mpfrcl  22399  selvval  22434  ply1frcl  22641  pnrmopn  23666  isi1f  26000  itg1val  26009  madeval  28223  axlowdimlem13  29537  axlowdim1  29542  ausgrusgri  29754  0uhgrsubgr  29865  cusgrsize  30040  ex-rn  31046  gidval  31119  grpoinvfval  31129  grpodivfval  31141  isablo  31153  vciOLD  31168  isvclem  31184  isnvlem  31217  isphg  31424  pj11i  32318  hmopidmch  32760  hmopidmpj  32761  pjss1coi  32770  padct  33357  tocyc01  33725  tocyccntz  33751  unitprodclb  33990  esplyfvaln  34252  esplyind  34253  locfinreflem  34518  locfinref  34519  issibf  35011  sitgfval  35019  onvf1odlem3  35952  mrsubvrs  36373  rdgprc0  36647  rdgprc  36648  dfrdg2  36649  brrangeg  36790  poimirlem24  38655  volsupnfl  38676  elghomlem1OLD  38912  isdivrngo  38977  iscom2  39022  elrefrels2  39623  elrefrels3  39624  refreleq  39626  elcnvrefrels2  39639  elcnvrefrels3  39640  dnnumch1  44144  aomclem3  44151  aomclem8  44156  rclexi  44708  rtrclex  44710  rtrclexi  44714  cnvrcl0  44718  dfrtrcl5  44722  dfrcl2  44767  csbima12gALTVD  45972  modelaxreplem1  46061  modelaxreplem2  46062  modelaxrep  46064  unirnmap  46314  ssmapsn  46322  sge0val  47469  vonvolmbl  47764