Theorem feq1 6685

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 6628	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5928	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3969	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 643	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6542	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6542	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ⊆ wss 3906  ran crn 5664   Fn wfn 6533  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  feq1d  6689  feq1i  6698  elimf  6706  f00  6762  f0bi  6763  f0dom0  6764  fconstg  6767  f1eq1  6771  fprb  7194  fconst2g  7203  fsnex  7283  orderseqlem  8154  soseq  8156  elmapg  8837  mapfset  8848  fsetsspwxp  8851  fsetfcdm  8858  fsetfocdm  8859  fsetprcnex  8860  ac6sfi  9245  updjud  9921  ac5num  10021  acni2  10031  cofsmo  10254  cfsmolem  10255  cfcoflem  10257  coftr  10258  alephsing  10261  axdc2lem  10433  axdc3lem2  10436  axdc3lem3  10437  axdc3  10439  axdc4lem  10440  ac6num  10464  inar1  10761  axdc4uzlem  14021  seqf1olem2  14080  seqf1o  14081  iswrd  14554  cshf1  14849  wrdlen2i  14981  ramub2  17075  ramcl  17090  isacs2  17710  isacs1i  17714  mreacs  17715  mgmb1mgm1  18714  elefmndbas2  18934  isgrpinv  19061  isghm  19287  islindf  21943  psdmul  22310  mat1dimelbas  22609  1stcfb  23583  upxp  23761  txcn  23764  isi1f  25814  mbfi1fseqlem6  25860  mbfi1flimlem  25862  itg2addlem  25898  plyf  26336  elno  27788  griedg0prc  29592  isgrpo  30827  vciOLD  30891  isvclem  30907  isnvlem  30940  ajmoi  31188  ajval  31191  hlimi  31518  chlimi  31564  chcompl  31572  adjmo  32162  adjeu  32219  adjval  32220  adj1  32263  adjeq  32265  cnlnssadj  32410  pjinvari  32521  padct  33041  locfinref  34209  isrnmeas  34568  filnetlem4  36870  bj-finsumval0  37907  poimirlem25  38274  poimirlem28  38277  volsupnfl  38294  mbfresfi  38295  upixp  38358  sdclem2  38371  sdclem1  38372  fdc  38374  ismgmOLD  38479  elghomlem2OLD  38515  istendo  41512  sticksstones1  42891  sticksstones2  42892  sticksstones3  42893  sticksstones8  42898  sticksstones9  42899  sticksstones10  42900  sticksstones11  42901  sticksstones12a  42902  sticksstones12  42903  sticksstones15  42906  sticksstones17  42908  sticksstones18  42909  sticksstones19  42910  sn-isghm  43385  ismrc  43412  relpeq1  45633  fmuldfeqlem1  46278  fmuldfeq  46279  dvnprodlem1  46640  stoweidlem15  46709  stoweidlem16  46710  stoweidlem17  46711  stoweidlem19  46713  stoweidlem20  46714  stoweidlem21  46715  stoweidlem22  46716  stoweidlem23  46717  stoweidlem27  46721  stoweidlem31  46725  stoweidlem32  46726  stoweidlem42  46736  stoweidlem48  46742  stoweidlem51  46745  stoweidlem59  46753  isomenndlem  47224  smfpimcclem  47501  fsetsniunop  47763  cfsetsnfsetf  47772  cfsetsnfsetf1  47773  cfsetsnfsetfo  47774  lincdifsn  49181  0aryfvalel  49391  mof0ALT  49595  mofsn  49599