Theorem feq1 6716

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ⊆ wss 3962  ran crn 5689   Fn wfn 6557  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-fun 6564  df-fn 6565  df-f 6566

This theorem is referenced by:  feq1d  6720  feq1i  6727  elimf  6735  f00  6790  f0bi  6791  f0dom0  6792  fconstg  6795  f1eq1  6799  fprb  7213  fconst2g  7222  fsnex  7302  orderseqlem  8180  soseq  8182  elmapg  8877  mapfset  8888  fsetsspwxp  8891  fsetfcdm  8898  fsetfocdm  8899  fsetprcnex  8900  ac6sfi  9317  updjud  9971  ac5num  10073  acni2  10083  cofsmo  10306  cfsmolem  10307  cfcoflem  10309  coftr  10310  alephsing  10313  axdc2lem  10485  axdc3lem2  10488  axdc3lem3  10489  axdc3  10491  axdc4lem  10492  ac6num  10516  inar1  10812  axdc4uzlem  14020  seqf1olem2  14079  seqf1o  14080  iswrd  14550  cshf1  14844  wrdlen2i  14977  ramub2  17047  ramcl  17062  isacs2  17697  isacs1i  17701  mreacs  17702  mgmb1mgm1  18680  elefmndbas2  18899  isgrpinv  19023  isghm  19245  isghmOLD  19246  islindf  21849  psdmul  22187  mat1dimelbas  22492  1stcfb  23468  upxp  23646  txcn  23649  isi1f  25722  mbfi1fseqlem6  25769  mbfi1flimlem  25771  itg2addlem  25807  plyf  26251  elno  27704  elnoOLD  27705  griedg0prc  29295  isgrpo  30525  vciOLD  30589  isvclem  30605  isnvlem  30638  ajmoi  30886  ajval  30889  hlimi  31216  chlimi  31262  chcompl  31270  adjmo  31860  adjeu  31917  adjval  31918  adj1  31961  adjeq  31963  cnlnssadj  32108  pjinvari  32219  padct  32736  locfinref  33801  isrnmeas  34180  filnetlem4  36363  bj-finsumval0  37267  poimirlem25  37631  poimirlem28  37634  volsupnfl  37651  mbfresfi  37652  upixp  37715  sdclem2  37728  sdclem1  37729  fdc  37731  ismgmOLD  37836  elghomlem2OLD  37872  istendo  40742  sticksstones1  42127  sticksstones2  42128  sticksstones3  42129  sticksstones8  42134  sticksstones9  42135  sticksstones10  42136  sticksstones11  42137  sticksstones12a  42138  sticksstones12  42139  sticksstones15  42142  sticksstones17  42144  sticksstones18  42145  sticksstones19  42146  sn-isghm  42659  ismrc  42688  fmuldfeqlem1  45537  fmuldfeq  45538  dvnprodlem1  45901  stoweidlem15  45970  stoweidlem16  45971  stoweidlem17  45972  stoweidlem19  45974  stoweidlem20  45975  stoweidlem21  45976  stoweidlem22  45977  stoweidlem23  45978  stoweidlem27  45982  stoweidlem31  45986  stoweidlem32  45987  stoweidlem42  45997  stoweidlem48  46003  stoweidlem51  46006  stoweidlem59  46014  isomenndlem  46485  smfpimcclem  46762  fsetsniunop  46998  cfsetsnfsetf  47007  cfsetsnfsetf1  47008  cfsetsnfsetfo  47009  lincdifsn  48269  0aryfvalel  48483  mof0ALT  48669  mofsn  48673