Theorem feq1 6691

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3931  ran crn 5660   Fn wfn 6531  ⟶wf 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  feq1d  6695  feq1i  6702  elimf  6710  f00  6765  f0bi  6766  f0dom0  6767  fconstg  6770  f1eq1  6774  fprb  7191  fconst2g  7200  fsnex  7281  orderseqlem  8161  soseq  8163  elmapg  8858  mapfset  8869  fsetsspwxp  8872  fsetfcdm  8879  fsetfocdm  8880  fsetprcnex  8881  ac6sfi  9297  updjud  9953  ac5num  10055  acni2  10065  cofsmo  10288  cfsmolem  10289  cfcoflem  10291  coftr  10292  alephsing  10295  axdc2lem  10467  axdc3lem2  10470  axdc3lem3  10471  axdc3  10473  axdc4lem  10474  ac6num  10498  inar1  10794  axdc4uzlem  14006  seqf1olem2  14065  seqf1o  14066  iswrd  14538  cshf1  14833  wrdlen2i  14966  ramub2  17039  ramcl  17054  isacs2  17670  isacs1i  17674  mreacs  17675  mgmb1mgm1  18638  elefmndbas2  18857  isgrpinv  18981  isghm  19203  isghmOLD  19204  islindf  21777  psdmul  22109  mat1dimelbas  22414  1stcfb  23388  upxp  23566  txcn  23569  isi1f  25632  mbfi1fseqlem6  25678  mbfi1flimlem  25680  itg2addlem  25716  plyf  26160  elno  27614  elnoOLD  27615  griedg0prc  29248  isgrpo  30483  vciOLD  30547  isvclem  30563  isnvlem  30596  ajmoi  30844  ajval  30847  hlimi  31174  chlimi  31220  chcompl  31228  adjmo  31818  adjeu  31875  adjval  31876  adj1  31919  adjeq  31921  cnlnssadj  32066  pjinvari  32177  padct  32702  locfinref  33877  isrnmeas  34236  filnetlem4  36404  bj-finsumval0  37308  poimirlem25  37674  poimirlem28  37677  volsupnfl  37694  mbfresfi  37695  upixp  37758  sdclem2  37771  sdclem1  37772  fdc  37774  ismgmOLD  37879  elghomlem2OLD  37915  istendo  40784  sticksstones1  42164  sticksstones2  42165  sticksstones3  42166  sticksstones8  42171  sticksstones9  42172  sticksstones10  42173  sticksstones11  42174  sticksstones12a  42175  sticksstones12  42176  sticksstones15  42179  sticksstones17  42181  sticksstones18  42182  sticksstones19  42183  sn-isghm  42671  ismrc  42699  relpeq1  44944  fmuldfeqlem1  45591  fmuldfeq  45592  dvnprodlem1  45955  stoweidlem15  46024  stoweidlem16  46025  stoweidlem17  46026  stoweidlem19  46028  stoweidlem20  46029  stoweidlem21  46030  stoweidlem22  46031  stoweidlem23  46032  stoweidlem27  46036  stoweidlem31  46040  stoweidlem32  46041  stoweidlem42  46051  stoweidlem48  46057  stoweidlem51  46060  stoweidlem59  46068  isomenndlem  46539  smfpimcclem  46816  fsetsniunop  47058  cfsetsnfsetf  47067  cfsetsnfsetf1  47068  cfsetsnfsetfo  47069  lincdifsn  48380  0aryfvalel  48594  mof0ALT  48798  mofsn  48802