Theorem feq1 6486

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 6430	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5780	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3909	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 634	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6344	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6344	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542   ⊆ wss 3844  ran crn 5527   Fn wfn 6335  ⟶wf 6336

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3401  df-un 3849  df-in 3851  df-ss 3861  df-sn 4518  df-pr 4520  df-op 4524  df-br 5032  df-opab 5094  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-fun 6342  df-fn 6343  df-f 6344

This theorem is referenced by:  feq1d  6490  feq1i  6496  elimf  6504  f00  6561  f0bi  6562  f0dom0  6563  fconstg  6566  f1eq1  6570  fprb  6969  fconst2g  6978  fsnex  7053  elmapg  8453  mapfset  8463  fsetsspwxp  8466  fsetfcdm  8473  fsetfocdm  8474  fsetprcnex  8475  ac6sfi  8839  updjud  9439  ac5num  9539  acni2  9549  cofsmo  9772  cfsmolem  9773  cfcoflem  9775  coftr  9776  alephsing  9779  axdc2lem  9951  axdc3lem2  9954  axdc3lem3  9955  axdc3  9957  axdc4lem  9958  ac6num  9982  inar1  10278  axdc4uzlem  13445  seqf1olem2  13505  seqf1o  13506  iswrd  13960  cshf1  14264  wrdlen2i  14396  ramub2  16453  ramcl  16468  isacs2  17030  isacs1i  17034  mreacs  17035  mgmb1mgm1  17984  elefmndbas2  18158  isgrpinv  18277  isghm  18479  islindf  20631  mat1dimelbas  21225  1stcfb  22199  upxp  22377  txcn  22380  isi1f  24429  mbfi1fseqlem6  24476  mbfi1flimlem  24478  itg2addlem  24514  plyf  24950  griedg0prc  27209  isgrpo  28435  vciOLD  28499  isvclem  28515  isnvlem  28548  ajmoi  28796  ajval  28799  hlimi  29126  chlimi  29172  chcompl  29180  adjmo  29770  adjeu  29827  adjval  29828  adj1  29871  adjeq  29873  cnlnssadj  30018  pjinvari  30129  padct  30632  locfinref  31366  isrnmeas  31741  orderseqlem  33417  soseq  33419  elno  33495  filnetlem4  34216  bj-finsumval0  35100  poimirlem25  35448  poimirlem28  35451  volsupnfl  35468  mbfresfi  35469  upixp  35533  sdclem2  35546  sdclem1  35547  fdc  35549  ismgmOLD  35654  elghomlem2OLD  35690  istendo  38420  sticksstones1  39731  sticksstones2  39732  sticksstones3  39733  sticksstones8  39738  ismrc  40118  fmuldfeqlem1  42688  fmuldfeq  42689  dvnprodlem1  43052  stoweidlem15  43121  stoweidlem16  43122  stoweidlem17  43123  stoweidlem19  43125  stoweidlem20  43126  stoweidlem21  43127  stoweidlem22  43128  stoweidlem23  43129  stoweidlem27  43133  stoweidlem31  43137  stoweidlem32  43138  stoweidlem42  43148  stoweidlem48  43154  stoweidlem51  43157  stoweidlem59  43165  isomenndlem  43633  smfpimcclem  43902  fsetsniunop  44105  cfsetsnfsetf  44114  cfsetsnfsetf1  44115  cfsetsnfsetfo  44116  lincdifsn  45329  0aryfvalel  45544  mof0ALT  45727  mofsn  45731