Theorem fneq1i 6634

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 6628	. 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)

Syntax hints:   ↔ wb 209   = wceq 1570   Fn wfn 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-fun 6540  df-fn 6541

This theorem is referenced by:  fnunop  6653  mptfnf  6672  fnopabg  6674  f1oun  6842  f1oiOLD  6862  f1osn  6864  ovid  7553  curry1  8100  curry2  8103  fsplitfpar  8114  frrlem11  8294  tfrlem10  8375  tfr1  8385  seqomlem2  8439  seqomlem3  8440  seqomlem4  8441  fnseqom  8443  unblem4  9256  r1fnon  9740  alephfnon  10050  alephfplem4  10092  alephfp  10093  cfsmolem  10255  infpssrlem3  10290  compssiso  10359  hsmexlem5  10415  axdclem2  10505  wunex2  10724  wuncval2  10733  om2uzrani  13990  om2uzf1oi  13991  uzrdglem  13995  uzrdgfni  13996  uzrdg0i  13997  hashkf  14370  dmaf  18107  cdaf  18108  prdsinvlem  19116  rng1zrlem  20260  pws1  20407  rngcrescrhm  20770  frlmphl  21912  ovolunlem1  25637  0plef  25812  0pledm  25813  itg1ge0  25826  mbfi1fseqlem5  25859  itg2addlem  25898  qaa  26465  precsexlem1  28381  precsexlem2  28382  precsexlem3  28383  precsexlem4  28384  precsexlem5  28385  ex-fpar  30794  0vfval  30939  xrge0pluscn  34311  bnj927  35139  bnj535  35259  fullfunfnv  36419  neibastop2lem  36852  fnmptif  45963  fourierdlem42  46846  cjnpoly  47609  fcoreslem4  47786  upgrimwlklem1  48645  rngcrescrhmALTV  49028  isofval2  49793