Theorem fneq1i 6676

Description: Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
fneq1i.1	⊢ 𝐹 = 𝐺

Assertion

Ref	Expression
fneq1i	⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)

Proof of Theorem fneq1i

Step	Hyp	Ref	Expression
1		fneq1i.1	. 2 ⊢ 𝐹 = 𝐺
2		fneq1 6670	. 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1537   Fn wfn 6568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-fun 6575  df-fn 6576

This theorem is referenced by:  fnunop  6695  mptfnf  6715  fnopabg  6717  f1oun  6881  f1oi  6900  f1osn  6902  ovid  7591  curry1  8145  curry2  8148  fsplitfpar  8159  frrlem11  8337  wfrlem5OLD  8369  wfrlem13OLD  8377  tfrlem10  8443  tfr1  8453  seqomlem2  8507  seqomlem3  8508  seqomlem4  8509  fnseqom  8511  unblem4  9359  r1fnon  9836  alephfnon  10134  alephfplem4  10176  alephfp  10177  cfsmolem  10339  infpssrlem3  10374  compssiso  10443  hsmexlem5  10499  axdclem2  10589  wunex2  10807  wuncval2  10816  om2uzrani  14003  om2uzf1oi  14004  uzrdglem  14008  uzrdgfni  14009  uzrdg0i  14010  hashkf  14381  dmaf  18116  cdaf  18117  prdsinvlem  19089  srg1zr  20242  pws1  20348  rngcrescrhm  20706  frlmphl  21824  ovolunlem1  25551  0plef  25726  0pledm  25727  itg1ge0  25740  itg1addlem4OLD  25754  mbfi1fseqlem5  25774  itg2addlem  25813  qaa  26383  precsexlem1  28249  precsexlem2  28250  precsexlem3  28251  precsexlem4  28252  precsexlem5  28253  ex-fpar  30494  0vfval  30638  xrge0pluscn  33886  bnj927  34745  bnj535  34866  fullfunfnv  35910  neibastop2lem  36326  fnmptif  45175  fourierdlem42  46070  fcoreslem4  46981  rngcrescrhmALTV  48003