Theorem feq1 6698

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 6640	. . 3 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
2		rneq 5933	. . . 4 ⊢ (𝐹 = 𝐺 → ran 𝐹 = ran 𝐺)
3	2	sseq1d 4010	. . 3 ⊢ (𝐹 = 𝐺 → (ran 𝐹 ⊆ 𝐵 ↔ ran 𝐺 ⊆ 𝐵))
4	1, 3	anbi12d 631	. 2 ⊢ (𝐹 = 𝐺 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵)))
5		df-f 6547	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
6		df-f 6547	. 2 ⊢ (𝐺:𝐴⟶𝐵 ↔ (𝐺 Fn 𝐴 ∧ ran 𝐺 ⊆ 𝐵))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ⊆ wss 3945  ran crn 5674   Fn wfn 6538  ⟶wf 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3429  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-br 5144  df-opab 5206  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-fun 6545  df-fn 6546  df-f 6547

This theorem is referenced by:  feq1d  6702  feq1i  6708  elimf  6716  f00  6774  f0bi  6775  f0dom0  6776  fconstg  6779  f1eq1  6783  fprb  7201  fconst2g  7210  fsnex  7287  orderseqlem  8157  soseq  8159  elmapg  8852  mapfset  8863  fsetsspwxp  8866  fsetfcdm  8873  fsetfocdm  8874  fsetprcnex  8875  ac6sfi  9306  updjud  9952  ac5num  10054  acni2  10064  cofsmo  10287  cfsmolem  10288  cfcoflem  10290  coftr  10291  alephsing  10294  axdc2lem  10466  axdc3lem2  10469  axdc3lem3  10470  axdc3  10472  axdc4lem  10473  ac6num  10497  inar1  10793  axdc4uzlem  13975  seqf1olem2  14034  seqf1o  14035  iswrd  14493  cshf1  14787  wrdlen2i  14920  ramub2  16977  ramcl  16992  isacs2  17627  isacs1i  17631  mreacs  17632  mgmb1mgm1  18609  elefmndbas2  18820  isgrpinv  18944  isghm  19164  islindf  21740  psdmul  22084  mat1dimelbas  22367  1stcfb  23343  upxp  23521  txcn  23524  isi1f  25597  mbfi1fseqlem6  25644  mbfi1flimlem  25646  itg2addlem  25682  plyf  26126  elno  27573  griedg0prc  29071  isgrpo  30301  vciOLD  30365  isvclem  30381  isnvlem  30414  ajmoi  30662  ajval  30665  hlimi  30992  chlimi  31038  chcompl  31046  adjmo  31636  adjeu  31693  adjval  31694  adj1  31737  adjeq  31739  cnlnssadj  31884  pjinvari  31995  padct  32496  locfinref  33437  isrnmeas  33814  filnetlem4  35860  bj-finsumval0  36759  poimirlem25  37113  poimirlem28  37116  volsupnfl  37133  mbfresfi  37134  upixp  37197  sdclem2  37210  sdclem1  37211  fdc  37213  ismgmOLD  37318  elghomlem2OLD  37354  istendo  40228  sticksstones1  41613  sticksstones2  41614  sticksstones3  41615  sticksstones8  41620  sticksstones9  41621  sticksstones10  41622  sticksstones11  41623  sticksstones12a  41624  sticksstones12  41625  sticksstones15  41628  sticksstones17  41630  sticksstones18  41631  sticksstones19  41632  ismrc  42112  fmuldfeqlem1  44961  fmuldfeq  44962  dvnprodlem1  45325  stoweidlem15  45394  stoweidlem16  45395  stoweidlem17  45396  stoweidlem19  45398  stoweidlem20  45399  stoweidlem21  45400  stoweidlem22  45401  stoweidlem23  45402  stoweidlem27  45406  stoweidlem31  45410  stoweidlem32  45411  stoweidlem42  45421  stoweidlem48  45427  stoweidlem51  45430  stoweidlem59  45438  isomenndlem  45909  smfpimcclem  46186  fsetsniunop  46422  cfsetsnfsetf  46431  cfsetsnfsetf1  46432  cfsetsnfsetfo  46433  lincdifsn  47483  0aryfvalel  47698  mof0ALT  47883  mofsn  47887

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »