Theorem feq1 6673

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 6616	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5917	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3970	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 643	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6529	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6529	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1563   ⊆ wss 3907  ran crn 5653   Fn wfn 6520  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-fun 6527  df-fn 6528  df-f 6529

This theorem is referenced by:  feq1d  6677  feq1i  6686  elimf  6694  f00  6750  f0bi  6751  f0dom0  6752  fconstg  6755  f1eq1  6759  fprb  7182  fconst2g  7191  fsnex  7271  orderseqlem  8141  soseq  8143  elmapg  8824  mapfset  8835  fsetsspwxp  8838  fsetfcdm  8845  fsetfocdm  8846  fsetprcnex  8847  ac6sfi  9232  updjud  9908  ac5num  10008  acni2  10018  cofsmo  10241  cfsmolem  10242  cfcoflem  10244  coftr  10245  alephsing  10248  axdc2lem  10420  axdc3lem2  10423  axdc3lem3  10424  axdc3  10426  axdc4lem  10427  ac6num  10451  inar1  10748  axdc4uzlem  14010  seqf1olem2  14069  seqf1o  14070  iswrd  14542  cshf1  14837  wrdlen2i  14969  ramub2  17064  ramcl  17079  isacs2  17699  isacs1i  17703  mreacs  17704  mgmb1mgm1  18703  elefmndbas2  18923  isgrpinv  19050  isghm  19277  islindf  21922  psdmul  22289  mat1dimelbas  22589  1stcfb  23563  upxp  23741  txcn  23744  isi1f  25794  mbfi1fseqlem6  25840  mbfi1flimlem  25842  itg2addlem  25878  plyf  26316  elno  27768  griedg0prc  29523  isgrpo  30758  vciOLD  30822  isvclem  30838  isnvlem  30871  ajmoi  31119  ajval  31122  hlimi  31449  chlimi  31495  chcompl  31503  adjmo  32093  adjeu  32150  adjval  32151  adj1  32194  adjeq  32196  cnlnssadj  32341  pjinvari  32452  padct  32975  locfinref  34148  isrnmeas  34507  filnetlem4  36754  bj-finsumval0  37789  poimirlem25  38156  poimirlem28  38159  volsupnfl  38176  mbfresfi  38177  upixp  38240  sdclem2  38253  sdclem1  38254  fdc  38256  ismgmOLD  38361  elghomlem2OLD  38397  istendo  41396  sticksstones1  42775  sticksstones2  42776  sticksstones3  42777  sticksstones8  42782  sticksstones9  42783  sticksstones10  42784  sticksstones11  42785  sticksstones12a  42786  sticksstones12  42787  sticksstones15  42790  sticksstones17  42792  sticksstones18  42793  sticksstones19  42794  sn-isghm  43267  ismrc  43294  relpeq1  45518  fmuldfeqlem1  46156  fmuldfeq  46157  dvnprodlem1  46518  stoweidlem15  46587  stoweidlem16  46588  stoweidlem17  46589  stoweidlem19  46591  stoweidlem20  46592  stoweidlem21  46593  stoweidlem22  46594  stoweidlem23  46595  stoweidlem27  46599  stoweidlem31  46603  stoweidlem32  46604  stoweidlem42  46614  stoweidlem48  46620  stoweidlem51  46623  stoweidlem59  46631  isomenndlem  47102  smfpimcclem  47379  fsetsniunop  47641  cfsetsnfsetf  47650  cfsetsnfsetf1  47651  cfsetsnfsetfo  47652  lincdifsn  49055  0aryfvalel  49265  mof0ALT  49469  mofsn  49473