Theorem feq1 6698

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 6640	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5935	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 4013	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 630	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6547	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6547	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1540   ⊆ wss 3948  ran crn 5677   Fn wfn 6538  ⟶wf 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-fun 6545  df-fn 6546  df-f 6547

This theorem is referenced by:  feq1d  6702  feq1i  6708  elimf  6716  f00  6773  f0bi  6774  f0dom0  6775  fconstg  6778  f1eq1  6782  fprb  7197  fconst2g  7206  fsnex  7284  orderseqlem  8148  soseq  8150  elmapg  8839  mapfset  8850  fsetsspwxp  8853  fsetfcdm  8860  fsetfocdm  8861  fsetprcnex  8862  ac6sfi  9293  updjud  9935  ac5num  10037  acni2  10047  cofsmo  10270  cfsmolem  10271  cfcoflem  10273  coftr  10274  alephsing  10277  axdc2lem  10449  axdc3lem2  10452  axdc3lem3  10453  axdc3  10455  axdc4lem  10456  ac6num  10480  inar1  10776  axdc4uzlem  13955  seqf1olem2  14015  seqf1o  14016  iswrd  14473  cshf1  14767  wrdlen2i  14900  ramub2  16954  ramcl  16969  isacs2  17604  isacs1i  17608  mreacs  17609  mgmb1mgm1  18586  elefmndbas2  18797  isgrpinv  18921  isghm  19137  islindf  21677  mat1dimelbas  22293  1stcfb  23269  upxp  23447  txcn  23450  isi1f  25523  mbfi1fseqlem6  25570  mbfi1flimlem  25572  itg2addlem  25608  plyf  26050  elno  27492  griedg0prc  28954  isgrpo  30183  vciOLD  30247  isvclem  30263  isnvlem  30296  ajmoi  30544  ajval  30547  hlimi  30874  chlimi  30920  chcompl  30928  adjmo  31518  adjeu  31575  adjval  31576  adj1  31619  adjeq  31621  cnlnssadj  31766  pjinvari  31877  padct  32377  locfinref  33285  isrnmeas  33662  filnetlem4  35730  bj-finsumval0  36630  poimirlem25  36977  poimirlem28  36980  volsupnfl  36997  mbfresfi  36998  upixp  37061  sdclem2  37074  sdclem1  37075  fdc  37077  ismgmOLD  37182  elghomlem2OLD  37218  istendo  40095  sticksstones1  41429  sticksstones2  41430  sticksstones3  41431  sticksstones8  41436  sticksstones9  41437  sticksstones10  41438  sticksstones11  41439  sticksstones12a  41440  sticksstones12  41441  sticksstones15  41444  sticksstones17  41446  sticksstones18  41447  sticksstones19  41448  ismrc  41902  fmuldfeqlem1  44757  fmuldfeq  44758  dvnprodlem1  45121  stoweidlem15  45190  stoweidlem16  45191  stoweidlem17  45192  stoweidlem19  45194  stoweidlem20  45195  stoweidlem21  45196  stoweidlem22  45197  stoweidlem23  45198  stoweidlem27  45202  stoweidlem31  45206  stoweidlem32  45207  stoweidlem42  45217  stoweidlem48  45223  stoweidlem51  45226  stoweidlem59  45234  isomenndlem  45705  smfpimcclem  45982  fsetsniunop  46218  cfsetsnfsetf  46227  cfsetsnfsetf1  46228  cfsetsnfsetfo  46229  lincdifsn  47267  0aryfvalel  47482  mof0ALT  47668  mofsn  47672