Theorem feq1 6272

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 6224	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5596	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3851	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 624	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6139	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6139	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 306	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1601   ⊆ wss 3792  ran crn 5356   Fn wfn 6130  ⟶wf 6131

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4887  df-opab 4949  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-fun 6137  df-fn 6138  df-f 6139

This theorem is referenced by:  feq1d  6276  feq1i  6282  elimf  6290  f00  6337  f0bi  6338  f0dom0  6339  fconstg  6342  f1eq1  6346  fprb  6731  fconst2g  6740  fsnex  6810  elmapg  8153  ac6sfi  8492  updjud  9093  ac5num  9192  acni2  9202  cofsmo  9426  cfsmolem  9427  cfcoflem  9429  coftr  9430  alephsing  9433  axdc2lem  9605  axdc3lem2  9608  axdc3lem3  9609  axdc3  9611  axdc4lem  9612  ac6num  9636  inar1  9932  axdc4uzlem  13101  seqf1olem2  13159  seqf1o  13160  iswrd  13601  cshf1  13961  wrdlen2i  14093  ramub2  16122  ramcl  16137  isacs2  16699  isacs1i  16703  mreacs  16704  mgmb1mgm1  17640  isgrpinv  17859  isghm  18044  islindf  20555  mat1dimelbas  20682  1stcfb  21657  upxp  21835  txcn  21838  isi1f  23878  mbfi1fseqlem6  23924  mbfi1flimlem  23926  itg2addlem  23962  plyf  24391  griedg0prc  26611  isgrpo  27924  vciOLD  27988  isvclem  28004  isnvlem  28037  ajmoi  28286  ajval  28289  hlimi  28617  chlimi  28663  chcompl  28671  adjmo  29263  adjeu  29320  adjval  29321  adj1  29364  adjeq  29366  cnlnssadj  29511  pjinvari  29622  padct  30063  locfinref  30506  isrnmeas  30861  orderseqlem  32341  soseq  32343  elno  32388  filnetlem4  32964  bj-finsumval0  33749  poimirlem25  34060  poimirlem28  34063  volsupnfl  34080  mbfresfi  34081  upixp  34149  sdclem2  34162  sdclem1  34163  fdc  34165  ismgmOLD  34273  elghomlem2OLD  34309  istendo  36914  ismrc  38224  fmuldfeqlem1  40722  fmuldfeq  40723  dvnprodlem1  41089  stoweidlem15  41159  stoweidlem16  41160  stoweidlem17  41161  stoweidlem19  41163  stoweidlem20  41164  stoweidlem21  41165  stoweidlem22  41166  stoweidlem23  41167  stoweidlem27  41171  stoweidlem31  41175  stoweidlem32  41176  stoweidlem42  41186  stoweidlem48  41192  stoweidlem51  41195  stoweidlem59  41203  isomenndlem  41671  smfpimcclem  41940  lincdifsn  43228