Theorem feq1 6697

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ⊆ wss 3944  ran crn 5673   Fn wfn 6537  ⟶wf 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-opab 5205  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-fun 6544  df-fn 6545  df-f 6546

This theorem is referenced by:  feq1d  6701  feq1i  6707  elimf  6715  f00  6773  f0bi  6774  f0dom0  6775  fconstg  6778  f1eq1  6782  fprb  7200  fconst2g  7209  fsnex  7286  orderseqlem  8156  soseq  8158  elmapg  8849  mapfset  8860  fsetsspwxp  8863  fsetfcdm  8870  fsetfocdm  8871  fsetprcnex  8872  ac6sfi  9303  updjud  9949  ac5num  10051  acni2  10061  cofsmo  10284  cfsmolem  10285  cfcoflem  10287  coftr  10288  alephsing  10291  axdc2lem  10463  axdc3lem2  10466  axdc3lem3  10467  axdc3  10469  axdc4lem  10470  ac6num  10494  inar1  10790  axdc4uzlem  13972  seqf1olem2  14031  seqf1o  14032  iswrd  14490  cshf1  14784  wrdlen2i  14917  ramub2  16974  ramcl  16989  isacs2  17624  isacs1i  17628  mreacs  17629  mgmb1mgm1  18606  elefmndbas2  18817  isgrpinv  18941  isghm  19161  islindf  21733  psdmul  22077  mat1dimelbas  22360  1stcfb  23336  upxp  23514  txcn  23517  isi1f  25590  mbfi1fseqlem6  25637  mbfi1flimlem  25639  itg2addlem  25675  plyf  26119  elno  27566  griedg0prc  29064  isgrpo  30294  vciOLD  30358  isvclem  30374  isnvlem  30407  ajmoi  30655  ajval  30658  hlimi  30985  chlimi  31031  chcompl  31039  adjmo  31629  adjeu  31686  adjval  31687  adj1  31730  adjeq  31732  cnlnssadj  31877  pjinvari  31988  padct  32485  locfinref  33378  isrnmeas  33755  filnetlem4  35801  bj-finsumval0  36700  poimirlem25  37053  poimirlem28  37056  volsupnfl  37073  mbfresfi  37074  upixp  37137  sdclem2  37150  sdclem1  37151  fdc  37153  ismgmOLD  37258  elghomlem2OLD  37294  istendo  40170  sticksstones1  41550  sticksstones2  41551  sticksstones3  41552  sticksstones8  41557  sticksstones9  41558  sticksstones10  41559  sticksstones11  41560  sticksstones12a  41561  sticksstones12  41562  sticksstones15  41565  sticksstones17  41567  sticksstones18  41568  sticksstones19  41569  ismrc  42043  fmuldfeqlem1  44893  fmuldfeq  44894  dvnprodlem1  45257  stoweidlem15  45326  stoweidlem16  45327  stoweidlem17  45328  stoweidlem19  45330  stoweidlem20  45331  stoweidlem21  45332  stoweidlem22  45333  stoweidlem23  45334  stoweidlem27  45338  stoweidlem31  45342  stoweidlem32  45343  stoweidlem42  45353  stoweidlem48  45359  stoweidlem51  45362  stoweidlem59  45370  isomenndlem  45841  smfpimcclem  46118  fsetsniunop  46354  cfsetsnfsetf  46363  cfsetsnfsetf1  46364  cfsetsnfsetfo  46365  lincdifsn  47415  0aryfvalel  47630  mof0ALT  47815  mofsn  47819