Theorem feq1 3620

Description: Equality theorem for functions.

Assertion

Ref	Expression
feq1	|- (F = G -> (F:A-->B <-> G:A-->B))

Proof of Theorem feq1

Step	Hyp	Ref	Expression
1		fneq1 3582	. . 3 |- (F = G -> (F Fn A <-> G Fn A))
2		rneq 3339	. . . 4 |- (F = G -> ran F = ran G)
3	2	sseq1d 2088	. . 3 |- (F = G -> (ran F (_ B <-> ran G (_ B))
4	1, 3	anbi12d 628	. 2 |- (F = G -> ((F Fn A /\ ran F (_ B) <-> (G Fn A /\ ran G (_ B)))
5		df-f 3194	. 2 |- (F:A-->B <-> (F Fn A /\ ran F (_ B))
6		df-f 3194	. 2 |- (G:A-->B <-> (G Fn A /\ ran G (_ B))
7	4, 5, 6	3bitr4g 555	1 |- (F = G -> (F:A-->B <-> G:A-->B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   (_ wss 2047  ran crn 3171   Fn wfn 3177  -->wf 3178

This theorem is referenced by:  feq1d 3624  elimf 3626  f00 3657  fconstg 3659  f1eq1 3660  fopab2 3823  fconst2g 3845  fconstfv 3849  elmapg 4333  map0 4344  pw2en 4446  ac6lem 4754  ser1ft 6328  climfnn 7092  caucvg3t 7168  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  elcncf 7265  acdc3lem 7486  acdc3 7487  acdc2lem2 7489  acdc2 7490  acdc5lem2 7492  acdc5 7493  acdclem 7494  acdc 7495  ruclem13 7522  ruclem17 7526  ismet 7798  ismsg 7800  msflem 7803  blf 7844  cnmet 7904  lmfex 7959  metelcls 7965  metcn4i 7972  iscms2lem5 7993  isgrp 8041  issubgi 8122  isring 8141  ringi 8142  vci 8167  isvclem 8196  isnvlem 8229  nvi 8233  islno 8414  ajmoi 8519  hcau 9051  hlim 9056  hlim2 9060  chlim 9104  chcompl 9115  ho0f 9677  adjmo 9758  elcnopt 9783  ellnopt 9784  elhmopt 9800  elcnfnt 9809  ellnfnt 9810  adjvalt 9814  adjt 9857  adjeqt 9859  cnlnssadj 10013  pjinvar 10119  stelt 10141  hstelt 10142  elghomlem2 10383  ismgra 10642  isalg 10653  algi 10660  isfunb 10755

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620  df-opab 2667  df-id 2835  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-fun 3192  df-fn 3193  df-f 3194

Copyright terms: Public domain