Theorem feq1 6590

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 6533	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5848	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3953	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 631	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6441	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6441	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ⊆ wss 3888  ran crn 5591   Fn wfn 6432  ⟶wf 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-fun 6439  df-fn 6440  df-f 6441

This theorem is referenced by:  feq1d  6594  feq1i  6600  elimf  6608  f00  6665  f0bi  6666  f0dom0  6667  fconstg  6670  f1eq1  6674  fprb  7078  fconst2g  7087  fsnex  7164  elmapg  8637  mapfset  8647  fsetsspwxp  8650  fsetfcdm  8657  fsetfocdm  8658  fsetprcnex  8659  ac6sfi  9067  updjud  9701  ac5num  9801  acni2  9811  cofsmo  10034  cfsmolem  10035  cfcoflem  10037  coftr  10038  alephsing  10041  axdc2lem  10213  axdc3lem2  10216  axdc3lem3  10217  axdc3  10219  axdc4lem  10220  ac6num  10244  inar1  10540  axdc4uzlem  13712  seqf1olem2  13772  seqf1o  13773  iswrd  14228  cshf1  14532  wrdlen2i  14664  ramub2  16724  ramcl  16739  isacs2  17371  isacs1i  17375  mreacs  17376  mgmb1mgm1  18348  elefmndbas2  18522  isgrpinv  18641  isghm  18843  islindf  21028  mat1dimelbas  21629  1stcfb  22605  upxp  22783  txcn  22786  isi1f  24847  mbfi1fseqlem6  24894  mbfi1flimlem  24896  itg2addlem  24932  plyf  25368  griedg0prc  27640  isgrpo  28868  vciOLD  28932  isvclem  28948  isnvlem  28981  ajmoi  29229  ajval  29232  hlimi  29559  chlimi  29605  chcompl  29613  adjmo  30203  adjeu  30260  adjval  30261  adj1  30304  adjeq  30306  cnlnssadj  30451  pjinvari  30562  padct  31063  locfinref  31800  isrnmeas  32177  orderseqlem  33810  soseq  33812  elno  33858  filnetlem4  34579  bj-finsumval0  35465  poimirlem25  35811  poimirlem28  35814  volsupnfl  35831  mbfresfi  35832  upixp  35896  sdclem2  35909  sdclem1  35910  fdc  35912  ismgmOLD  36017  elghomlem2OLD  36053  istendo  38781  sticksstones1  40109  sticksstones2  40110  sticksstones3  40111  sticksstones8  40116  sticksstones9  40117  sticksstones10  40118  sticksstones11  40119  sticksstones12a  40120  sticksstones12  40121  sticksstones15  40124  sticksstones17  40126  sticksstones18  40127  sticksstones19  40128  ismrc  40530  fmuldfeqlem1  43130  fmuldfeq  43131  dvnprodlem1  43494  stoweidlem15  43563  stoweidlem16  43564  stoweidlem17  43565  stoweidlem19  43567  stoweidlem20  43568  stoweidlem21  43569  stoweidlem22  43570  stoweidlem23  43571  stoweidlem27  43575  stoweidlem31  43579  stoweidlem32  43580  stoweidlem42  43590  stoweidlem48  43596  stoweidlem51  43599  stoweidlem59  43607  isomenndlem  44075  smfpimcclem  44351  fsetsniunop  44554  cfsetsnfsetf  44563  cfsetsnfsetf1  44564  cfsetsnfsetfo  44565  lincdifsn  45776  0aryfvalel  45991  mof0ALT  46178  mofsn  46182