Theorem feq1 6690

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 6633	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5931	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3971	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6547	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6547	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ⊆ wss 3908  ran crn 5667   Fn wfn 6538  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  feq1d  6694  feq1i  6703  elimf  6711  f00  6767  f0bi  6768  f0dom0  6769  fconstg  6772  f1eq1  6776  fprb  7199  fconst2g  7208  fsnex  7292  orderseqlem  8162  soseq  8164  elmapg  8845  mapfset  8856  fsetsspwxp  8859  fsetfcdm  8866  fsetfocdm  8867  fsetprcnex  8868  ac6sfi  9254  updjud  9939  ac5num  10039  acni2  10049  cofsmo  10271  cfsmolem  10272  cfcoflem  10274  coftr  10275  alephsing  10278  axdc2lem  10450  axdc3lem2  10453  axdc3lem3  10454  axdc3  10456  axdc4lem  10457  ac6num  10481  inar1  10778  axdc4uzlem  14039  seqf1olem2  14098  seqf1o  14099  iswrd  14572  cshf1  14873  wrdlen2i  15005  ramub2  17099  ramcl  17114  isacs2  17734  isacs1i  17738  mreacs  17739  mgmb1mgm1  18738  elefmndbas2  18964  isgrpinv  19091  isghm  19317  islindf  21999  psdmul  22366  mat1dimelbas  22665  1stcfb  23639  upxp  23817  txcn  23820  isi1f  25870  mbfi1fseqlem6  25916  mbfi1flimlem  25918  itg2addlem  25954  plyf  26392  elno  27847  griedg0prc  29651  isgrpo  30886  vciOLD  30950  isvclem  30966  isnvlem  30999  ajmoi  31247  ajval  31250  hlimi  31577  chlimi  31623  chcompl  31631  adjmo  32221  adjeu  32278  adjval  32279  adj1  32322  adjeq  32324  cnlnssadj  32469  pjinvari  32580  padct  33100  locfinref  34262  isrnmeas  34622  filnetlem4  36933  bj-finsumval0  37970  poimirlem25  38337  poimirlem28  38340  volsupnfl  38357  mbfresfi  38358  upixp  38421  sdclem2  38434  sdclem1  38435  fdc  38437  ismgmOLD  38542  elghomlem2OLD  38578  istendo  41575  sticksstones1  42954  sticksstones2  42955  sticksstones3  42956  sticksstones8  42961  sticksstones9  42962  sticksstones10  42963  sticksstones11  42964  sticksstones12a  42965  sticksstones12  42966  sticksstones15  42969  sticksstones17  42971  sticksstones18  42972  sticksstones19  42973  sn-isghm  43446  ismrc  43473  relpeq1  45694  fmuldfeqlem1  46339  fmuldfeq  46340  dvnprodlem1  46701  stoweidlem15  46770  stoweidlem16  46771  stoweidlem17  46772  stoweidlem19  46774  stoweidlem20  46775  stoweidlem21  46776  stoweidlem22  46777  stoweidlem23  46778  stoweidlem27  46782  stoweidlem31  46786  stoweidlem32  46787  stoweidlem42  46797  stoweidlem48  46803  stoweidlem51  46806  stoweidlem59  46814  isomenndlem  47285  smfpimcclem  47562  fsetsniunop  47827  cfsetsnfsetf  47836  cfsetsnfsetf1  47837  cfsetsnfsetfo  47838  lincdifsn  49245  0aryfvalel  49455  mof0ALT  49659  mofsn  49663