Theorem feq1 6646

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 6589	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5891	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3953	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6502	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6502	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ⊆ wss 3889  ran crn 5632   Fn wfn 6493  ⟶wf 6494

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6500  df-fn 6501  df-f 6502

This theorem is referenced by:  feq1d  6650  feq1i  6659  elimf  6667  f00  6722  f0bi  6723  f0dom0  6724  fconstg  6727  f1eq1  6731  fprb  7149  fconst2g  7158  fsnex  7238  orderseqlem  8107  soseq  8109  elmapg  8786  mapfset  8797  fsetsspwxp  8800  fsetfcdm  8807  fsetfocdm  8808  fsetprcnex  8809  ac6sfi  9194  updjud  9858  ac5num  9958  acni2  9968  cofsmo  10191  cfsmolem  10192  cfcoflem  10194  coftr  10195  alephsing  10198  axdc2lem  10370  axdc3lem2  10373  axdc3lem3  10374  axdc3  10376  axdc4lem  10377  ac6num  10401  inar1  10698  axdc4uzlem  13945  seqf1olem2  14004  seqf1o  14005  iswrd  14477  cshf1  14772  wrdlen2i  14904  ramub2  16985  ramcl  17000  isacs2  17619  isacs1i  17623  mreacs  17624  mgmb1mgm1  18623  elefmndbas2  18842  isgrpinv  18969  isghm  19190  isghmOLD  19191  islindf  21792  psdmul  22132  mat1dimelbas  22436  1stcfb  23410  upxp  23588  txcn  23591  isi1f  25641  mbfi1fseqlem6  25687  mbfi1flimlem  25689  itg2addlem  25725  plyf  26163  elno  27609  elnoOLD  27610  griedg0prc  29333  isgrpo  30568  vciOLD  30632  isvclem  30648  isnvlem  30681  ajmoi  30929  ajval  30932  hlimi  31259  chlimi  31305  chcompl  31313  adjmo  31903  adjeu  31960  adjval  31961  adj1  32004  adjeq  32006  cnlnssadj  32151  pjinvari  32262  padct  32791  locfinref  33985  isrnmeas  34344  filnetlem4  36563  bj-finsumval0  37599  poimirlem25  37966  poimirlem28  37969  volsupnfl  37986  mbfresfi  37987  upixp  38050  sdclem2  38063  sdclem1  38064  fdc  38066  ismgmOLD  38171  elghomlem2OLD  38207  istendo  41206  sticksstones1  42585  sticksstones2  42586  sticksstones3  42587  sticksstones8  42592  sticksstones9  42593  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones12  42597  sticksstones15  42600  sticksstones17  42602  sticksstones18  42603  sticksstones19  42604  sn-isghm  43106  ismrc  43133  relpeq1  45371  fmuldfeqlem1  46012  fmuldfeq  46013  dvnprodlem1  46374  stoweidlem15  46443  stoweidlem16  46444  stoweidlem17  46445  stoweidlem19  46447  stoweidlem20  46448  stoweidlem21  46449  stoweidlem22  46450  stoweidlem23  46451  stoweidlem27  46455  stoweidlem31  46459  stoweidlem32  46460  stoweidlem42  46470  stoweidlem48  46476  stoweidlem51  46479  stoweidlem59  46487  isomenndlem  46958  smfpimcclem  47235  fsetsniunop  47497  cfsetsnfsetf  47506  cfsetsnfsetf1  47507  cfsetsnfsetfo  47508  lincdifsn  48900  0aryfvalel  49110  mof0ALT  49315  mofsn  49319