Theorem feq1 6715

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ⊆ wss 3950  ran crn 5685   Fn wfn 6555  ⟶wf 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-fun 6562  df-fn 6563  df-f 6564

This theorem is referenced by:  feq1d  6719  feq1i  6726  elimf  6734  f00  6789  f0bi  6790  f0dom0  6791  fconstg  6794  f1eq1  6798  fprb  7215  fconst2g  7224  fsnex  7304  orderseqlem  8183  soseq  8185  elmapg  8880  mapfset  8891  fsetsspwxp  8894  fsetfcdm  8901  fsetfocdm  8902  fsetprcnex  8903  ac6sfi  9321  updjud  9975  ac5num  10077  acni2  10087  cofsmo  10310  cfsmolem  10311  cfcoflem  10313  coftr  10314  alephsing  10317  axdc2lem  10489  axdc3lem2  10492  axdc3lem3  10493  axdc3  10495  axdc4lem  10496  ac6num  10520  inar1  10816  axdc4uzlem  14025  seqf1olem2  14084  seqf1o  14085  iswrd  14555  cshf1  14849  wrdlen2i  14982  ramub2  17053  ramcl  17068  isacs2  17697  isacs1i  17701  mreacs  17702  mgmb1mgm1  18669  elefmndbas2  18888  isgrpinv  19012  isghm  19234  isghmOLD  19235  islindf  21833  psdmul  22171  mat1dimelbas  22478  1stcfb  23454  upxp  23632  txcn  23635  isi1f  25710  mbfi1fseqlem6  25756  mbfi1flimlem  25758  itg2addlem  25794  plyf  26238  elno  27691  elnoOLD  27692  griedg0prc  29282  isgrpo  30517  vciOLD  30581  isvclem  30597  isnvlem  30630  ajmoi  30878  ajval  30881  hlimi  31208  chlimi  31254  chcompl  31262  adjmo  31852  adjeu  31909  adjval  31910  adj1  31953  adjeq  31955  cnlnssadj  32100  pjinvari  32211  padct  32732  locfinref  33841  isrnmeas  34202  filnetlem4  36383  bj-finsumval0  37287  poimirlem25  37653  poimirlem28  37656  volsupnfl  37673  mbfresfi  37674  upixp  37737  sdclem2  37750  sdclem1  37751  fdc  37753  ismgmOLD  37858  elghomlem2OLD  37894  istendo  40763  sticksstones1  42148  sticksstones2  42149  sticksstones3  42150  sticksstones8  42155  sticksstones9  42156  sticksstones10  42157  sticksstones11  42158  sticksstones12a  42159  sticksstones12  42160  sticksstones15  42163  sticksstones17  42165  sticksstones18  42166  sticksstones19  42167  sn-isghm  42688  ismrc  42717  relpeq1  44970  fmuldfeqlem1  45602  fmuldfeq  45603  dvnprodlem1  45966  stoweidlem15  46035  stoweidlem16  46036  stoweidlem17  46037  stoweidlem19  46039  stoweidlem20  46040  stoweidlem21  46041  stoweidlem22  46042  stoweidlem23  46043  stoweidlem27  46047  stoweidlem31  46051  stoweidlem32  46052  stoweidlem42  46062  stoweidlem48  46068  stoweidlem51  46071  stoweidlem59  46079  isomenndlem  46550  smfpimcclem  46827  fsetsniunop  47066  cfsetsnfsetf  47075  cfsetsnfsetf1  47076  cfsetsnfsetfo  47077  lincdifsn  48346  0aryfvalel  48560  mof0ALT  48754  mofsn  48758