Theorem feq1 6629

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ⊆ wss 3902  ran crn 5617   Fn wfn 6476  ⟶wf 6477

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-fun 6483  df-fn 6484  df-f 6485

This theorem is referenced by:  feq1d  6633  feq1i  6642  elimf  6650  f00  6705  f0bi  6706  f0dom0  6707  fconstg  6710  f1eq1  6714  fprb  7128  fconst2g  7137  fsnex  7217  orderseqlem  8087  soseq  8089  elmapg  8763  mapfset  8774  fsetsspwxp  8777  fsetfcdm  8784  fsetfocdm  8785  fsetprcnex  8786  ac6sfi  9168  updjud  9824  ac5num  9924  acni2  9934  cofsmo  10157  cfsmolem  10158  cfcoflem  10160  coftr  10161  alephsing  10164  axdc2lem  10336  axdc3lem2  10339  axdc3lem3  10340  axdc3  10342  axdc4lem  10343  ac6num  10367  inar1  10663  axdc4uzlem  13887  seqf1olem2  13946  seqf1o  13947  iswrd  14419  cshf1  14714  wrdlen2i  14846  ramub2  16923  ramcl  16938  isacs2  17556  isacs1i  17560  mreacs  17561  mgmb1mgm1  18560  elefmndbas2  18779  isgrpinv  18903  isghm  19125  isghmOLD  19126  islindf  21747  psdmul  22079  mat1dimelbas  22384  1stcfb  23358  upxp  23536  txcn  23539  isi1f  25600  mbfi1fseqlem6  25646  mbfi1flimlem  25648  itg2addlem  25684  plyf  26128  elno  27582  elnoOLD  27583  griedg0prc  29240  isgrpo  30472  vciOLD  30536  isvclem  30552  isnvlem  30585  ajmoi  30833  ajval  30836  hlimi  31163  chlimi  31209  chcompl  31217  adjmo  31807  adjeu  31864  adjval  31865  adj1  31908  adjeq  31910  cnlnssadj  32055  pjinvari  32166  padct  32696  locfinref  33849  isrnmeas  34208  filnetlem4  36414  bj-finsumval0  37318  poimirlem25  37684  poimirlem28  37687  volsupnfl  37704  mbfresfi  37705  upixp  37768  sdclem2  37781  sdclem1  37782  fdc  37784  ismgmOLD  37889  elghomlem2OLD  37925  istendo  40798  sticksstones1  42178  sticksstones2  42179  sticksstones3  42180  sticksstones8  42185  sticksstones9  42186  sticksstones10  42187  sticksstones11  42188  sticksstones12a  42189  sticksstones12  42190  sticksstones15  42193  sticksstones17  42195  sticksstones18  42196  sticksstones19  42197  sn-isghm  42705  ismrc  42733  relpeq1  44976  fmuldfeqlem1  45621  fmuldfeq  45622  dvnprodlem1  45983  stoweidlem15  46052  stoweidlem16  46053  stoweidlem17  46054  stoweidlem19  46056  stoweidlem20  46057  stoweidlem21  46058  stoweidlem22  46059  stoweidlem23  46060  stoweidlem27  46064  stoweidlem31  46068  stoweidlem32  46069  stoweidlem42  46079  stoweidlem48  46085  stoweidlem51  46088  stoweidlem59  46096  isomenndlem  46567  smfpimcclem  46844  fsetsniunop  47079  cfsetsnfsetf  47088  cfsetsnfsetf1  47089  cfsetsnfsetfo  47090  lincdifsn  48455  0aryfvalel  48665  mof0ALT  48870  mofsn  48874