Theorem feq1 6489

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 6438	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5800	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3997	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6353	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6353	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 316	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ⊆ wss 3935  ran crn 5550   Fn wfn 6344  ⟶wf 6345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-br 5059  df-opab 5121  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-fun 6351  df-fn 6352  df-f 6353

This theorem is referenced by:  feq1d  6493  feq1i  6499  elimf  6507  f00  6555  f0bi  6556  f0dom0  6557  fconstg  6560  f1eq1  6564  fprb  6950  fconst2g  6959  fsnex  7033  elmapg  8413  ac6sfi  8756  updjud  9357  ac5num  9456  acni2  9466  cofsmo  9685  cfsmolem  9686  cfcoflem  9688  coftr  9689  alephsing  9692  axdc2lem  9864  axdc3lem2  9867  axdc3lem3  9868  axdc3  9870  axdc4lem  9871  ac6num  9895  inar1  10191  axdc4uzlem  13345  seqf1olem2  13404  seqf1o  13405  iswrd  13857  cshf1  14166  wrdlen2i  14298  ramub2  16344  ramcl  16359  isacs2  16918  isacs1i  16922  mreacs  16923  mgmb1mgm1  17859  elefmndbas2  18033  isgrpinv  18150  isghm  18352  islindf  20950  mat1dimelbas  21074  1stcfb  22047  upxp  22225  txcn  22228  isi1f  24269  mbfi1fseqlem6  24315  mbfi1flimlem  24317  itg2addlem  24353  plyf  24782  griedg0prc  27040  isgrpo  28268  vciOLD  28332  isvclem  28348  isnvlem  28381  ajmoi  28629  ajval  28632  hlimi  28959  chlimi  29005  chcompl  29013  adjmo  29603  adjeu  29660  adjval  29661  adj1  29704  adjeq  29706  cnlnssadj  29851  pjinvari  29962  padct  30449  locfinref  31100  isrnmeas  31454  orderseqlem  33089  soseq  33091  elno  33148  filnetlem4  33724  bj-finsumval0  34561  poimirlem25  34911  poimirlem28  34914  volsupnfl  34931  mbfresfi  34932  upixp  34998  sdclem2  35011  sdclem1  35012  fdc  35014  ismgmOLD  35122  elghomlem2OLD  35158  istendo  37890  ismrc  39291  fmuldfeqlem1  41856  fmuldfeq  41857  dvnprodlem1  42224  stoweidlem15  42294  stoweidlem16  42295  stoweidlem17  42296  stoweidlem19  42298  stoweidlem20  42299  stoweidlem21  42300  stoweidlem22  42301  stoweidlem23  42302  stoweidlem27  42306  stoweidlem31  42310  stoweidlem32  42311  stoweidlem42  42321  stoweidlem48  42327  stoweidlem51  42330  stoweidlem59  42338  isomenndlem  42806  smfpimcclem  43075  lincdifsn  44473