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 3954	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 633	. 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 1542   ⊆ wss 3890  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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  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  7142  fconst2g  7151  fsnex  7231  orderseqlem  8100  soseq  8102  elmapg  8779  mapfset  8790  fsetsspwxp  8793  fsetfcdm  8800  fsetfocdm  8801  fsetprcnex  8802  ac6sfi  9187  updjud  9849  ac5num  9949  acni2  9959  cofsmo  10182  cfsmolem  10183  cfcoflem  10185  coftr  10186  alephsing  10189  axdc2lem  10361  axdc3lem2  10364  axdc3lem3  10365  axdc3  10367  axdc4lem  10368  ac6num  10392  inar1  10689  axdc4uzlem  13936  seqf1olem2  13995  seqf1o  13996  iswrd  14468  cshf1  14763  wrdlen2i  14895  ramub2  16976  ramcl  16991  isacs2  17610  isacs1i  17614  mreacs  17615  mgmb1mgm1  18614  elefmndbas2  18833  isgrpinv  18960  isghm  19181  isghmOLD  19182  islindf  21802  psdmul  22142  mat1dimelbas  22446  1stcfb  23420  upxp  23598  txcn  23601  isi1f  25651  mbfi1fseqlem6  25697  mbfi1flimlem  25699  itg2addlem  25735  plyf  26173  elno  27623  elnoOLD  27624  griedg0prc  29347  isgrpo  30583  vciOLD  30647  isvclem  30663  isnvlem  30696  ajmoi  30944  ajval  30947  hlimi  31274  chlimi  31320  chcompl  31328  adjmo  31918  adjeu  31975  adjval  31976  adj1  32019  adjeq  32021  cnlnssadj  32166  pjinvari  32277  padct  32806  locfinref  34001  isrnmeas  34360  filnetlem4  36579  bj-finsumval0  37615  poimirlem25  37980  poimirlem28  37983  volsupnfl  38000  mbfresfi  38001  upixp  38064  sdclem2  38077  sdclem1  38078  fdc  38080  ismgmOLD  38185  elghomlem2OLD  38221  istendo  41220  sticksstones1  42599  sticksstones2  42600  sticksstones3  42601  sticksstones8  42606  sticksstones9  42607  sticksstones10  42608  sticksstones11  42609  sticksstones12a  42610  sticksstones12  42611  sticksstones15  42614  sticksstones17  42616  sticksstones18  42617  sticksstones19  42618  sn-isghm  43120  ismrc  43147  relpeq1  45389  fmuldfeqlem1  46030  fmuldfeq  46031  dvnprodlem1  46392  stoweidlem15  46461  stoweidlem16  46462  stoweidlem17  46463  stoweidlem19  46465  stoweidlem20  46466  stoweidlem21  46467  stoweidlem22  46468  stoweidlem23  46469  stoweidlem27  46473  stoweidlem31  46477  stoweidlem32  46478  stoweidlem42  46488  stoweidlem48  46494  stoweidlem51  46497  stoweidlem59  46505  isomenndlem  46976  smfpimcclem  47253  fsetsniunop  47509  cfsetsnfsetf  47518  cfsetsnfsetf1  47519  cfsetsnfsetfo  47520  lincdifsn  48912  0aryfvalel  49122  mof0ALT  49327  mofsn  49331