Theorem feq1 6640

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ⊆ wss 3901  ran crn 5625   Fn wfn 6487  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  feq1d  6644  feq1i  6653  elimf  6661  f00  6716  f0bi  6717  f0dom0  6718  fconstg  6721  f1eq1  6725  fprb  7140  fconst2g  7149  fsnex  7229  orderseqlem  8099  soseq  8101  elmapg  8776  mapfset  8787  fsetsspwxp  8790  fsetfcdm  8797  fsetfocdm  8798  fsetprcnex  8799  ac6sfi  9184  updjud  9846  ac5num  9946  acni2  9956  cofsmo  10179  cfsmolem  10180  cfcoflem  10182  coftr  10183  alephsing  10186  axdc2lem  10358  axdc3lem2  10361  axdc3lem3  10362  axdc3  10364  axdc4lem  10365  ac6num  10389  inar1  10686  axdc4uzlem  13906  seqf1olem2  13965  seqf1o  13966  iswrd  14438  cshf1  14733  wrdlen2i  14865  ramub2  16942  ramcl  16957  isacs2  17576  isacs1i  17580  mreacs  17581  mgmb1mgm1  18580  elefmndbas2  18799  isgrpinv  18923  isghm  19144  isghmOLD  19145  islindf  21767  psdmul  22109  mat1dimelbas  22415  1stcfb  23389  upxp  23567  txcn  23570  isi1f  25631  mbfi1fseqlem6  25677  mbfi1flimlem  25679  itg2addlem  25715  plyf  26159  elno  27613  elnoOLD  27614  griedg0prc  29337  isgrpo  30572  vciOLD  30636  isvclem  30652  isnvlem  30685  ajmoi  30933  ajval  30936  hlimi  31263  chlimi  31309  chcompl  31317  adjmo  31907  adjeu  31964  adjval  31965  adj1  32008  adjeq  32010  cnlnssadj  32155  pjinvari  32266  padct  32797  locfinref  33998  isrnmeas  34357  filnetlem4  36575  bj-finsumval0  37486  poimirlem25  37842  poimirlem28  37845  volsupnfl  37862  mbfresfi  37863  upixp  37926  sdclem2  37939  sdclem1  37940  fdc  37942  ismgmOLD  38047  elghomlem2OLD  38083  istendo  41016  sticksstones1  42396  sticksstones2  42397  sticksstones3  42398  sticksstones8  42403  sticksstones9  42404  sticksstones10  42405  sticksstones11  42406  sticksstones12a  42407  sticksstones12  42408  sticksstones15  42411  sticksstones17  42413  sticksstones18  42414  sticksstones19  42415  sn-isghm  42912  ismrc  42939  relpeq1  45181  fmuldfeqlem1  45824  fmuldfeq  45825  dvnprodlem1  46186  stoweidlem15  46255  stoweidlem16  46256  stoweidlem17  46257  stoweidlem19  46259  stoweidlem20  46260  stoweidlem21  46261  stoweidlem22  46262  stoweidlem23  46263  stoweidlem27  46267  stoweidlem31  46271  stoweidlem32  46272  stoweidlem42  46282  stoweidlem48  46288  stoweidlem51  46291  stoweidlem59  46299  isomenndlem  46770  smfpimcclem  47047  fsetsniunop  47291  cfsetsnfsetf  47300  cfsetsnfsetf1  47301  cfsetsnfsetfo  47302  lincdifsn  48666  0aryfvalel  48876  mof0ALT  49081  mofsn  49085