Theorem feq1d 5349

Description: Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)

Hypothesis

Ref	Expression
feq1d.1	|- ( ph -> F = G )

Assertion

Ref	Expression
feq1d	|- ( ph -> ( F : A --> B <-> G : A --> B ) )

Proof of Theorem feq1d

Step	Hyp	Ref	Expression
1		feq1d.1	. 2 |- ( ph -> F = G )
2		feq1 5345	. 2 |- ( F = G -> ( F : A --> B <-> G : A --> B ) )
3	1, 2	syl 14	1 |- ( ph -> ( F : A --> B <-> G : A --> B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   -->wf 5209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-br 4002  df-opab 4063  df-rel 4631  df-cnv 4632  df-co 4633  df-dm 4634  df-rn 4635  df-fun 5215  df-fn 5216  df-f 5217

This theorem is referenced by:  feq12d  5352  fco2  5379  fssres2  5390  fresin  5391  fmpt3d  5669  fmptco  5679  fressnfv  5700  off  6090  caofinvl  6100  f2ndf  6222  eroprf  6623  pmresg  6671  fseq1p1m1  10087  mgmplusf  12715  mgmb1mgm1  12717  grpsubf  12877  lmbr  13495  blfps  13691  blf  13692  dvmptclx  13962  lgsfcl3  14204