Theorem feq1 6696

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ⊆ wss 3948  ran crn 5677   Fn wfn 6536  ⟶wf 6537

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  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 6543  df-fn 6544  df-f 6545

This theorem is referenced by:  feq1d  6700  feq1i  6706  elimf  6714  f00  6771  f0bi  6772  f0dom0  6773  fconstg  6776  f1eq1  6780  fprb  7192  fconst2g  7201  fsnex  7278  orderseqlem  8140  soseq  8142  elmapg  8830  mapfset  8841  fsetsspwxp  8844  fsetfcdm  8851  fsetfocdm  8852  fsetprcnex  8853  ac6sfi  9284  updjud  9926  ac5num  10028  acni2  10038  cofsmo  10261  cfsmolem  10262  cfcoflem  10264  coftr  10265  alephsing  10268  axdc2lem  10440  axdc3lem2  10443  axdc3lem3  10444  axdc3  10446  axdc4lem  10447  ac6num  10471  inar1  10767  axdc4uzlem  13945  seqf1olem2  14005  seqf1o  14006  iswrd  14463  cshf1  14757  wrdlen2i  14890  ramub2  16944  ramcl  16959  isacs2  17594  isacs1i  17598  mreacs  17599  mgmb1mgm1  18571  elefmndbas2  18752  isgrpinv  18875  isghm  19087  islindf  21359  mat1dimelbas  21965  1stcfb  22941  upxp  23119  txcn  23122  isi1f  25183  mbfi1fseqlem6  25230  mbfi1flimlem  25232  itg2addlem  25268  plyf  25704  elno  27139  griedg0prc  28511  isgrpo  29738  vciOLD  29802  isvclem  29818  isnvlem  29851  ajmoi  30099  ajval  30102  hlimi  30429  chlimi  30475  chcompl  30483  adjmo  31073  adjeu  31130  adjval  31131  adj1  31174  adjeq  31176  cnlnssadj  31321  pjinvari  31432  padct  31932  locfinref  32810  isrnmeas  33187  filnetlem4  35255  bj-finsumval0  36155  poimirlem25  36502  poimirlem28  36505  volsupnfl  36522  mbfresfi  36523  upixp  36586  sdclem2  36599  sdclem1  36600  fdc  36602  ismgmOLD  36707  elghomlem2OLD  36743  istendo  39620  sticksstones1  40951  sticksstones2  40952  sticksstones3  40953  sticksstones8  40958  sticksstones9  40959  sticksstones10  40960  sticksstones11  40961  sticksstones12a  40962  sticksstones12  40963  sticksstones15  40966  sticksstones17  40968  sticksstones18  40969  sticksstones19  40970  ismrc  41425  fmuldfeqlem1  44285  fmuldfeq  44286  dvnprodlem1  44649  stoweidlem15  44718  stoweidlem16  44719  stoweidlem17  44720  stoweidlem19  44722  stoweidlem20  44723  stoweidlem21  44724  stoweidlem22  44725  stoweidlem23  44726  stoweidlem27  44730  stoweidlem31  44734  stoweidlem32  44735  stoweidlem42  44745  stoweidlem48  44751  stoweidlem51  44754  stoweidlem59  44762  isomenndlem  45233  smfpimcclem  45510  fsetsniunop  45746  cfsetsnfsetf  45755  cfsetsnfsetf1  45756  cfsetsnfsetfo  45757  lincdifsn  47059  0aryfvalel  47274  mof0ALT  47460  mofsn  47464