Theorem feq1 6666

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ⊆ wss 3914  ran crn 5639   Fn wfn 6506  ⟶wf 6507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  feq1d  6670  feq1i  6679  elimf  6687  f00  6742  f0bi  6743  f0dom0  6744  fconstg  6747  f1eq1  6751  fprb  7168  fconst2g  7177  fsnex  7258  orderseqlem  8136  soseq  8138  elmapg  8812  mapfset  8823  fsetsspwxp  8826  fsetfcdm  8833  fsetfocdm  8834  fsetprcnex  8835  ac6sfi  9231  updjud  9887  ac5num  9989  acni2  9999  cofsmo  10222  cfsmolem  10223  cfcoflem  10225  coftr  10226  alephsing  10229  axdc2lem  10401  axdc3lem2  10404  axdc3lem3  10405  axdc3  10407  axdc4lem  10408  ac6num  10432  inar1  10728  axdc4uzlem  13948  seqf1olem2  14007  seqf1o  14008  iswrd  14480  cshf1  14775  wrdlen2i  14908  ramub2  16985  ramcl  17000  isacs2  17614  isacs1i  17618  mreacs  17619  mgmb1mgm1  18582  elefmndbas2  18801  isgrpinv  18925  isghm  19147  isghmOLD  19148  islindf  21721  psdmul  22053  mat1dimelbas  22358  1stcfb  23332  upxp  23510  txcn  23513  isi1f  25575  mbfi1fseqlem6  25621  mbfi1flimlem  25623  itg2addlem  25659  plyf  26103  elno  27557  elnoOLD  27558  griedg0prc  29191  isgrpo  30426  vciOLD  30490  isvclem  30506  isnvlem  30539  ajmoi  30787  ajval  30790  hlimi  31117  chlimi  31163  chcompl  31171  adjmo  31761  adjeu  31818  adjval  31819  adj1  31862  adjeq  31864  cnlnssadj  32009  pjinvari  32120  padct  32643  locfinref  33831  isrnmeas  34190  filnetlem4  36369  bj-finsumval0  37273  poimirlem25  37639  poimirlem28  37642  volsupnfl  37659  mbfresfi  37660  upixp  37723  sdclem2  37736  sdclem1  37737  fdc  37739  ismgmOLD  37844  elghomlem2OLD  37880  istendo  40754  sticksstones1  42134  sticksstones2  42135  sticksstones3  42136  sticksstones8  42141  sticksstones9  42142  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones12  42146  sticksstones15  42149  sticksstones17  42151  sticksstones18  42152  sticksstones19  42153  sn-isghm  42661  ismrc  42689  relpeq1  44934  fmuldfeqlem1  45580  fmuldfeq  45581  dvnprodlem1  45944  stoweidlem15  46013  stoweidlem16  46014  stoweidlem17  46015  stoweidlem19  46017  stoweidlem20  46018  stoweidlem21  46019  stoweidlem22  46020  stoweidlem23  46021  stoweidlem27  46025  stoweidlem31  46029  stoweidlem32  46030  stoweidlem42  46040  stoweidlem48  46046  stoweidlem51  46049  stoweidlem59  46057  isomenndlem  46528  smfpimcclem  46805  fsetsniunop  47050  cfsetsnfsetf  47059  cfsetsnfsetf1  47060  cfsetsnfsetfo  47061  lincdifsn  48413  0aryfvalel  48623  mof0ALT  48828  mofsn  48832