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 3953	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 638	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6496	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6496	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 315	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ⊆ wss 3890  ran crn 5626   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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  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  7145  fconst2g  7154  fsnex  7234  orderseqlem  8104  soseq  8106  elmapg  8783  mapfset  8794  fsetsspwxp  8797  fsetfcdm  8804  fsetfocdm  8805  fsetprcnex  8806  ac6sfi  9191  updjud  9856  ac5num  9956  acni2  9966  cofsmo  10189  cfsmolem  10190  cfcoflem  10192  coftr  10193  alephsing  10196  axdc2lem  10368  axdc3lem2  10371  axdc3lem3  10372  axdc3  10374  axdc4lem  10375  ac6num  10399  inar1  10696  axdc4uzlem  13943  seqf1olem2  14002  seqf1o  14003  iswrd  14475  cshf1  14770  wrdlen2i  14902  ramub2  16983  ramcl  16998  isacs2  17617  isacs1i  17621  mreacs  17622  mgmb1mgm1  18621  elefmndbas2  18840  isgrpinv  18967  isghm  19188  isghmOLD  19189  islindf  21794  psdmul  22161  mat1dimelbas  22461  1stcfb  23435  upxp  23613  txcn  23616  isi1f  25666  mbfi1fseqlem6  25712  mbfi1flimlem  25714  itg2addlem  25750  plyf  26188  elno  27634  elnoOLD  27635  griedg0prc  29358  isgrpo  30593  vciOLD  30657  isvclem  30673  isnvlem  30706  ajmoi  30954  ajval  30957  hlimi  31284  chlimi  31330  chcompl  31338  adjmo  31928  adjeu  31985  adjval  31986  adj1  32029  adjeq  32031  cnlnssadj  32176  pjinvari  32287  padct  32817  locfinref  34032  isrnmeas  34391  filnetlem4  36616  bj-finsumval0  37652  poimirlem25  38019  poimirlem28  38022  volsupnfl  38039  mbfresfi  38040  upixp  38103  sdclem2  38116  sdclem1  38117  fdc  38119  ismgmOLD  38224  elghomlem2OLD  38260  istendo  41259  sticksstones1  42638  sticksstones2  42639  sticksstones3  42640  sticksstones8  42645  sticksstones9  42646  sticksstones10  42647  sticksstones11  42648  sticksstones12a  42649  sticksstones12  42650  sticksstones15  42653  sticksstones17  42655  sticksstones18  42656  sticksstones19  42657  sn-isghm  43130  ismrc  43157  relpeq1  45395  fmuldfeqlem1  46034  fmuldfeq  46035  dvnprodlem1  46396  stoweidlem15  46465  stoweidlem16  46466  stoweidlem17  46467  stoweidlem19  46469  stoweidlem20  46470  stoweidlem21  46471  stoweidlem22  46472  stoweidlem23  46473  stoweidlem27  46477  stoweidlem31  46481  stoweidlem32  46482  stoweidlem42  46492  stoweidlem48  46498  stoweidlem51  46501  stoweidlem59  46509  isomenndlem  46980  smfpimcclem  47257  fsetsniunop  47519  cfsetsnfsetf  47528  cfsetsnfsetf1  47529  cfsetsnfsetfo  47530  lincdifsn  48922  0aryfvalel  49132  mof0ALT  49337  mofsn  49341