Theorem feq1 6648

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 6591	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5893	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 3967	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6504	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6504	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ⊆ wss 3903  ran crn 5633   Fn wfn 6495  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  feq1d  6652  feq1i  6661  elimf  6669  f00  6724  f0bi  6725  f0dom0  6726  fconstg  6729  f1eq1  6733  fprb  7150  fconst2g  7159  fsnex  7239  orderseqlem  8109  soseq  8111  elmapg  8788  mapfset  8799  fsetsspwxp  8802  fsetfcdm  8809  fsetfocdm  8810  fsetprcnex  8811  ac6sfi  9196  updjud  9858  ac5num  9958  acni2  9968  cofsmo  10191  cfsmolem  10192  cfcoflem  10194  coftr  10195  alephsing  10198  axdc2lem  10370  axdc3lem2  10373  axdc3lem3  10374  axdc3  10376  axdc4lem  10377  ac6num  10401  inar1  10698  axdc4uzlem  13918  seqf1olem2  13977  seqf1o  13978  iswrd  14450  cshf1  14745  wrdlen2i  14877  ramub2  16954  ramcl  16969  isacs2  17588  isacs1i  17592  mreacs  17593  mgmb1mgm1  18592  elefmndbas2  18811  isgrpinv  18935  isghm  19156  isghmOLD  19157  islindf  21779  psdmul  22121  mat1dimelbas  22427  1stcfb  23401  upxp  23579  txcn  23582  isi1f  25643  mbfi1fseqlem6  25689  mbfi1flimlem  25691  itg2addlem  25727  plyf  26171  elno  27625  elnoOLD  27626  griedg0prc  29349  isgrpo  30584  vciOLD  30648  isvclem  30664  isnvlem  30697  ajmoi  30945  ajval  30948  hlimi  31275  chlimi  31321  chcompl  31329  adjmo  31919  adjeu  31976  adjval  31977  adj1  32020  adjeq  32022  cnlnssadj  32167  pjinvari  32278  padct  32807  locfinref  34018  isrnmeas  34377  filnetlem4  36594  bj-finsumval0  37534  poimirlem25  37890  poimirlem28  37893  volsupnfl  37910  mbfresfi  37911  upixp  37974  sdclem2  37987  sdclem1  37988  fdc  37990  ismgmOLD  38095  elghomlem2OLD  38131  istendo  41130  sticksstones1  42510  sticksstones2  42511  sticksstones3  42512  sticksstones8  42517  sticksstones9  42518  sticksstones10  42519  sticksstones11  42520  sticksstones12a  42521  sticksstones12  42522  sticksstones15  42525  sticksstones17  42527  sticksstones18  42528  sticksstones19  42529  sn-isghm  43025  ismrc  43052  relpeq1  45294  fmuldfeqlem1  45936  fmuldfeq  45937  dvnprodlem1  46298  stoweidlem15  46367  stoweidlem16  46368  stoweidlem17  46369  stoweidlem19  46371  stoweidlem20  46372  stoweidlem21  46373  stoweidlem22  46374  stoweidlem23  46375  stoweidlem27  46379  stoweidlem31  46383  stoweidlem32  46384  stoweidlem42  46394  stoweidlem48  46400  stoweidlem51  46403  stoweidlem59  46411  isomenndlem  46882  smfpimcclem  47159  fsetsniunop  47403  cfsetsnfsetf  47412  cfsetsnfsetf1  47413  cfsetsnfsetfo  47414  lincdifsn  48778  0aryfvalel  48988  mof0ALT  49193  mofsn  49197