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 5875	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3961	. . 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 3897  ran crn 5615   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 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  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  9827  ac5num  9927  acni2  9937  cofsmo  10160  cfsmolem  10161  cfcoflem  10163  coftr  10164  alephsing  10167  axdc2lem  10339  axdc3lem2  10342  axdc3lem3  10343  axdc3  10345  axdc4lem  10346  ac6num  10370  inar1  10666  axdc4uzlem  13890  seqf1olem2  13949  seqf1o  13950  iswrd  14422  cshf1  14717  wrdlen2i  14849  ramub2  16926  ramcl  16941  isacs2  17559  isacs1i  17563  mreacs  17564  mgmb1mgm1  18563  elefmndbas2  18782  isgrpinv  18906  isghm  19127  isghmOLD  19128  islindf  21749  psdmul  22081  mat1dimelbas  22386  1stcfb  23360  upxp  23538  txcn  23541  isi1f  25602  mbfi1fseqlem6  25648  mbfi1flimlem  25650  itg2addlem  25686  plyf  26130  elno  27584  elnoOLD  27585  griedg0prc  29242  isgrpo  30477  vciOLD  30541  isvclem  30557  isnvlem  30590  ajmoi  30838  ajval  30841  hlimi  31168  chlimi  31214  chcompl  31222  adjmo  31812  adjeu  31869  adjval  31870  adj1  31913  adjeq  31915  cnlnssadj  32060  pjinvari  32171  padct  32701  locfinref  33854  isrnmeas  34213  filnetlem4  36425  bj-finsumval0  37329  poimirlem25  37684  poimirlem28  37687  volsupnfl  37704  mbfresfi  37705  upixp  37768  sdclem2  37781  sdclem1  37782  fdc  37784  ismgmOLD  37889  elghomlem2OLD  37925  istendo  40858  sticksstones1  42238  sticksstones2  42239  sticksstones3  42240  sticksstones8  42245  sticksstones9  42246  sticksstones10  42247  sticksstones11  42248  sticksstones12a  42249  sticksstones12  42250  sticksstones15  42253  sticksstones17  42255  sticksstones18  42256  sticksstones19  42257  sn-isghm  42765  ismrc  42793  relpeq1  45036  fmuldfeqlem1  45681  fmuldfeq  45682  dvnprodlem1  46043  stoweidlem15  46112  stoweidlem16  46113  stoweidlem17  46114  stoweidlem19  46116  stoweidlem20  46117  stoweidlem21  46118  stoweidlem22  46119  stoweidlem23  46120  stoweidlem27  46124  stoweidlem31  46128  stoweidlem32  46129  stoweidlem42  46139  stoweidlem48  46145  stoweidlem51  46148  stoweidlem59  46156  isomenndlem  46627  smfpimcclem  46904  fsetsniunop  47148  cfsetsnfsetf  47157  cfsetsnfsetf1  47158  cfsetsnfsetfo  47159  lincdifsn  48524  0aryfvalel  48734  mof0ALT  48939  mofsn  48943