Theorem feq1 6699

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 6641	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5936	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 4014	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6548	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6548	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ⊆ wss 3949  ran crn 5678   Fn wfn 6539  ⟶wf 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-fun 6546  df-fn 6547  df-f 6548

This theorem is referenced by:  feq1d  6703  feq1i  6709  elimf  6717  f00  6774  f0bi  6775  f0dom0  6776  fconstg  6779  f1eq1  6783  fprb  7195  fconst2g  7204  fsnex  7281  orderseqlem  8143  soseq  8145  elmapg  8833  mapfset  8844  fsetsspwxp  8847  fsetfcdm  8854  fsetfocdm  8855  fsetprcnex  8856  ac6sfi  9287  updjud  9929  ac5num  10031  acni2  10041  cofsmo  10264  cfsmolem  10265  cfcoflem  10267  coftr  10268  alephsing  10271  axdc2lem  10443  axdc3lem2  10446  axdc3lem3  10447  axdc3  10449  axdc4lem  10450  ac6num  10474  inar1  10770  axdc4uzlem  13948  seqf1olem2  14008  seqf1o  14009  iswrd  14466  cshf1  14760  wrdlen2i  14893  ramub2  16947  ramcl  16962  isacs2  17597  isacs1i  17601  mreacs  17602  mgmb1mgm1  18574  elefmndbas2  18755  isgrpinv  18878  isghm  19092  islindf  21367  mat1dimelbas  21973  1stcfb  22949  upxp  23127  txcn  23130  isi1f  25191  mbfi1fseqlem6  25238  mbfi1flimlem  25240  itg2addlem  25276  plyf  25712  elno  27149  griedg0prc  28521  isgrpo  29750  vciOLD  29814  isvclem  29830  isnvlem  29863  ajmoi  30111  ajval  30114  hlimi  30441  chlimi  30487  chcompl  30495  adjmo  31085  adjeu  31142  adjval  31143  adj1  31186  adjeq  31188  cnlnssadj  31333  pjinvari  31444  padct  31944  locfinref  32821  isrnmeas  33198  filnetlem4  35266  bj-finsumval0  36166  poimirlem25  36513  poimirlem28  36516  volsupnfl  36533  mbfresfi  36534  upixp  36597  sdclem2  36610  sdclem1  36611  fdc  36613  ismgmOLD  36718  elghomlem2OLD  36754  istendo  39631  sticksstones1  40962  sticksstones2  40963  sticksstones3  40964  sticksstones8  40969  sticksstones9  40970  sticksstones10  40971  sticksstones11  40972  sticksstones12a  40973  sticksstones12  40974  sticksstones15  40977  sticksstones17  40979  sticksstones18  40980  sticksstones19  40981  ismrc  41439  fmuldfeqlem1  44298  fmuldfeq  44299  dvnprodlem1  44662  stoweidlem15  44731  stoweidlem16  44732  stoweidlem17  44733  stoweidlem19  44735  stoweidlem20  44736  stoweidlem21  44737  stoweidlem22  44738  stoweidlem23  44739  stoweidlem27  44743  stoweidlem31  44747  stoweidlem32  44748  stoweidlem42  44758  stoweidlem48  44764  stoweidlem51  44767  stoweidlem59  44775  isomenndlem  45246  smfpimcclem  45523  fsetsniunop  45759  cfsetsnfsetf  45768  cfsetsnfsetf1  45769  cfsetsnfsetfo  45770  lincdifsn  47105  0aryfvalel  47320  mof0ALT  47506  mofsn  47510