Theorem feq1 6709

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 6652	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5925	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3944	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6562	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6562	. 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 3900  ran crn 5656   Fn wfn 6553  ⟶wf 6554

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6560  df-fn 6561  df-f 6562

This theorem is used by:  feq1d  6713  feq1i  6722  elimf  6730  f00  6786  f0bi  6787  f0dom0  6788  fconstg  6791  f1eq1  6795  fprb  7222  fconst2g  7232  fsnex  7314  orderseqlem  8201  soseq  8203  elmapg  8887  mapfset  8900  fsetsspwxp  8903  fsetfcdm  8910  fsetfocdm  8911  fsetprcnex  8912  ac6sfi  9303  updjud  10042  ac5num  10142  acni2  10152  cofsmo  10374  cfsmolem  10375  cfcoflem  10377  coftr  10378  alephsing  10381  axdc2lem  10553  axdc3lem2  10556  axdc3lem3  10557  axdc3  10559  axdc4lem  10560  ac6num  10584  inar1  10887  axdc4uzlem  14153  seqf1olem2  14212  seqf1o  14213  iswrd  14687  cshf1  14989  wrdlen2i  15122  ramub2  17221  ramcl  17236  isacs2  17856  isacs1i  17860  mreacs  17861  mgmb1mgm1  18862  elefmndbas2  19099  isgrpinv  19233  isghm  19459  islindf  22148  psdmul  22517  mat1dimelbas  22816  1stcfb  23793  upxp  23972  txcn  23975  isi1f  26025  mbfi1fseqlem6  26071  mbfi1flimlem  26073  itg2addlem  26109  plyf  26546  elno  28033  griedg0prc  29875  isgrpo  31129  vciOLD  31193  isvclem  31209  isnvlem  31242  ajmoi  31490  ajval  31493  hlimi  31820  chlimi  31866  chcompl  31874  adjmo  32464  adjeu  32521  adjval  32522  adj1  32565  adjeq  32567  cnlnssadj  32712  pjinvari  32823  padct  33381  locfinref  34543  isrnmeas  34903  filnetlem4  37347  bj-finsumval0  38398  poimirlem25  38755  poimirlem28  38758  volsupnfl  38775  mbfresfi  38776  upixp  38855  sdclem2  38868  sdclem1  38869  fdc  38871  ismgmOLD  38976  elghomlem2OLD  39012  istendo  42009  sticksstones1  43388  sticksstones2  43389  sticksstones3  43390  sticksstones8  43395  sticksstones9  43396  sticksstones10  43397  sticksstones11  43398  sticksstones12a  43399  sticksstones12  43400  sticksstones15  43403  sticksstones17  43405  sticksstones18  43406  sticksstones19  43407  sn-isghm  43877  ismrc  43905  relpeq1  46129  fmuldfeqlem1  46799  fmuldfeq  46800  dvnprodlem1  47161  stoweidlem15  47230  stoweidlem16  47231  stoweidlem17  47232  stoweidlem19  47234  stoweidlem20  47235  stoweidlem21  47236  stoweidlem22  47237  stoweidlem23  47238  stoweidlem27  47242  stoweidlem31  47246  stoweidlem32  47247  stoweidlem42  47257  stoweidlem48  47263  stoweidlem51  47266  stoweidlem59  47274  isomenndlem  47745  smfpimcclem  48022  fsetsniunop  48324  cfsetsnfsetf  48333  cfsetsnfsetf1  48334  cfsetsnfsetfo  48335  lincdifsn  49741  0aryfvalel  49951  mof0ALT  50156  mofsn  50160