Theorem feq1 6679

Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
feq1	⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Proof of Theorem feq1

Step	Hyp	Ref	Expression
1		fneq1 6622	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5918	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3962	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6535	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6535	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ⊆ wss 3899  ran crn 5652   Fn wfn 6526  ⟶wf 6527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6533  df-fn 6534  df-f 6535

This theorem is used by:  feq1d  6683  feq1i  6692  elimf  6700  f00  6756  f0bi  6757  f0dom0  6758  fconstg  6761  f1eq1  6765  fprb  7191  fconst2g  7201  fsnex  7283  orderseqlem  8158  soseq  8160  elmapg  8843  mapfset  8856  fsetsspwxp  8859  fsetfcdm  8866  fsetfocdm  8867  fsetprcnex  8868  ac6sfi  9259  updjud  9996  ac5num  10096  acni2  10106  cofsmo  10328  cfsmolem  10329  cfcoflem  10331  coftr  10332  alephsing  10335  axdc2lem  10507  axdc3lem2  10510  axdc3lem3  10511  axdc3  10513  axdc4lem  10514  ac6num  10538  inar1  10841  axdc4uzlem  14106  seqf1olem2  14165  seqf1o  14166  iswrd  14640  cshf1  14941  wrdlen2i  15073  ramub2  17172  ramcl  17187  isacs2  17807  isacs1i  17811  mreacs  17812  mgmb1mgm1  18813  elefmndbas2  19050  isgrpinv  19184  isghm  19410  islindf  22098  psdmul  22467  mat1dimelbas  22766  1stcfb  23743  upxp  23922  txcn  23925  isi1f  25975  mbfi1fseqlem6  26021  mbfi1flimlem  26023  itg2addlem  26059  plyf  26496  elno  27985  griedg0prc  29827  isgrpo  31081  vciOLD  31145  isvclem  31161  isnvlem  31194  ajmoi  31442  ajval  31445  hlimi  31772  chlimi  31818  chcompl  31826  adjmo  32416  adjeu  32473  adjval  32474  adj1  32517  adjeq  32519  cnlnssadj  32664  pjinvari  32775  padct  33292  locfinref  34455  isrnmeas  34815  filnetlem4  37139  bj-finsumval0  38174  poimirlem25  38531  poimirlem28  38534  volsupnfl  38551  mbfresfi  38552  upixp  38631  sdclem2  38644  sdclem1  38645  fdc  38647  ismgmOLD  38752  elghomlem2OLD  38788  istendo  41785  sticksstones1  43164  sticksstones2  43165  sticksstones3  43166  sticksstones8  43171  sticksstones9  43172  sticksstones10  43173  sticksstones11  43174  sticksstones12a  43175  sticksstones12  43176  sticksstones15  43179  sticksstones17  43181  sticksstones18  43182  sticksstones19  43183  sn-isghm  43638  ismrc  43665  relpeq1  45886  fmuldfeqlem1  46538  fmuldfeq  46539  dvnprodlem1  46900  stoweidlem15  46969  stoweidlem16  46970  stoweidlem17  46971  stoweidlem19  46973  stoweidlem20  46974  stoweidlem21  46975  stoweidlem22  46976  stoweidlem23  46977  stoweidlem27  46981  stoweidlem31  46985  stoweidlem32  46986  stoweidlem42  46996  stoweidlem48  47002  stoweidlem51  47005  stoweidlem59  47013  isomenndlem  47484  smfpimcclem  47761  fsetsniunop  48063  cfsetsnfsetf  48072  cfsetsnfsetf1  48073  cfsetsnfsetfo  48074  lincdifsn  49480  0aryfvalel  49690  mof0ALT  49894  mofsn  49898