Theorem feq1 6565

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 6508	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5834	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3948	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 630	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6422	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6422	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 313	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ⊆ wss 3883  ran crn 5581   Fn wfn 6413  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  feq1d  6569  feq1i  6575  elimf  6583  f00  6640  f0bi  6641  f0dom0  6642  fconstg  6645  f1eq1  6649  fprb  7051  fconst2g  7060  fsnex  7135  elmapg  8586  mapfset  8596  fsetsspwxp  8599  fsetfcdm  8606  fsetfocdm  8607  fsetprcnex  8608  ac6sfi  8988  updjud  9623  ac5num  9723  acni2  9733  cofsmo  9956  cfsmolem  9957  cfcoflem  9959  coftr  9960  alephsing  9963  axdc2lem  10135  axdc3lem2  10138  axdc3lem3  10139  axdc3  10141  axdc4lem  10142  ac6num  10166  inar1  10462  axdc4uzlem  13631  seqf1olem2  13691  seqf1o  13692  iswrd  14147  cshf1  14451  wrdlen2i  14583  ramub2  16643  ramcl  16658  isacs2  17279  isacs1i  17283  mreacs  17284  mgmb1mgm1  18254  elefmndbas2  18428  isgrpinv  18547  isghm  18749  islindf  20929  mat1dimelbas  21528  1stcfb  22504  upxp  22682  txcn  22685  isi1f  24743  mbfi1fseqlem6  24790  mbfi1flimlem  24792  itg2addlem  24828  plyf  25264  griedg0prc  27534  isgrpo  28760  vciOLD  28824  isvclem  28840  isnvlem  28873  ajmoi  29121  ajval  29124  hlimi  29451  chlimi  29497  chcompl  29505  adjmo  30095  adjeu  30152  adjval  30153  adj1  30196  adjeq  30198  cnlnssadj  30343  pjinvari  30454  padct  30956  locfinref  31693  isrnmeas  32068  orderseqlem  33728  soseq  33730  elno  33776  filnetlem4  34497  bj-finsumval0  35383  poimirlem25  35729  poimirlem28  35732  volsupnfl  35749  mbfresfi  35750  upixp  35814  sdclem2  35827  sdclem1  35828  fdc  35830  ismgmOLD  35935  elghomlem2OLD  35971  istendo  38701  sticksstones1  40030  sticksstones2  40031  sticksstones3  40032  sticksstones8  40037  sticksstones9  40038  sticksstones10  40039  sticksstones11  40040  sticksstones12a  40041  sticksstones12  40042  sticksstones15  40045  sticksstones17  40047  sticksstones18  40048  sticksstones19  40049  ismrc  40439  fmuldfeqlem1  43013  fmuldfeq  43014  dvnprodlem1  43377  stoweidlem15  43446  stoweidlem16  43447  stoweidlem17  43448  stoweidlem19  43450  stoweidlem20  43451  stoweidlem21  43452  stoweidlem22  43453  stoweidlem23  43454  stoweidlem27  43458  stoweidlem31  43462  stoweidlem32  43463  stoweidlem42  43473  stoweidlem48  43479  stoweidlem51  43482  stoweidlem59  43490  isomenndlem  43958  smfpimcclem  44227  fsetsniunop  44430  cfsetsnfsetf  44439  cfsetsnfsetf1  44440  cfsetsnfsetfo  44441  lincdifsn  45653  0aryfvalel  45868  mof0ALT  46055  mofsn  46059