Theorem feq1 6468

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 6414	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5770	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3946	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6328	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6328	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ⊆ wss 3881  ran crn 5520   Fn wfn 6319  ⟶wf 6320

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-fun 6326  df-fn 6327  df-f 6328

This theorem is referenced by:  feq1d  6472  feq1i  6478  elimf  6486  f00  6535  f0bi  6536  f0dom0  6537  fconstg  6540  f1eq1  6544  fprb  6933  fconst2g  6942  fsnex  7017  elmapg  8402  ac6sfi  8746  updjud  9347  ac5num  9447  acni2  9457  cofsmo  9680  cfsmolem  9681  cfcoflem  9683  coftr  9684  alephsing  9687  axdc2lem  9859  axdc3lem2  9862  axdc3lem3  9863  axdc3  9865  axdc4lem  9866  ac6num  9890  inar1  10186  axdc4uzlem  13346  seqf1olem2  13406  seqf1o  13407  iswrd  13859  cshf1  14163  wrdlen2i  14295  ramub2  16340  ramcl  16355  isacs2  16916  isacs1i  16920  mreacs  16921  mgmb1mgm1  17857  elefmndbas2  18031  isgrpinv  18148  isghm  18350  islindf  20501  mat1dimelbas  21076  1stcfb  22050  upxp  22228  txcn  22231  isi1f  24278  mbfi1fseqlem6  24324  mbfi1flimlem  24326  itg2addlem  24362  plyf  24795  griedg0prc  27054  isgrpo  28280  vciOLD  28344  isvclem  28360  isnvlem  28393  ajmoi  28641  ajval  28644  hlimi  28971  chlimi  29017  chcompl  29025  adjmo  29615  adjeu  29672  adjval  29673  adj1  29716  adjeq  29718  cnlnssadj  29863  pjinvari  29974  padct  30481  locfinref  31194  isrnmeas  31569  orderseqlem  33207  soseq  33209  elno  33266  filnetlem4  33842  bj-finsumval0  34700  poimirlem25  35082  poimirlem28  35085  volsupnfl  35102  mbfresfi  35103  upixp  35167  sdclem2  35180  sdclem1  35181  fdc  35183  ismgmOLD  35288  elghomlem2OLD  35324  istendo  38056  ismrc  39642  fmuldfeqlem1  42224  fmuldfeq  42225  dvnprodlem1  42588  stoweidlem15  42657  stoweidlem16  42658  stoweidlem17  42659  stoweidlem19  42661  stoweidlem20  42662  stoweidlem21  42663  stoweidlem22  42664  stoweidlem23  42665  stoweidlem27  42669  stoweidlem31  42673  stoweidlem32  42674  stoweidlem42  42684  stoweidlem48  42690  stoweidlem51  42693  stoweidlem59  42701  isomenndlem  43169  smfpimcclem  43438  lincdifsn  44833  0aryfvalel  45048