Theorem fneq1i 6633

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   Fn wfn 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-fun 6539  df-fn 6540

This theorem is used by:  fnunop  6652  mptfnf  6671  fnopabg  6673  f1oun  6841  f1oiOLD  6861  f1osn  6863  ovid  7558  curry1  8105  curry2  8108  fsplitfpar  8119  frrlem11  8299  tfrlem10  8380  tfr1  8390  seqomlem2  8444  seqomlem3  8445  seqomlem4  8446  fnseqom  8448  unblem4  9269  r1fnon  9753  alephfnon  10072  alephfplem4  10114  alephfp  10115  cfsmolem  10276  infpssrlem3  10311  compssiso  10380  hsmexlem5  10436  axdclem2  10526  wunex2  10751  wuncval2  10760  om2uzrani  14020  om2uzf1oi  14021  uzrdglem  14025  uzrdgfni  14026  uzrdg0i  14027  hashkf  14400  dmaf  18144  cdaf  18145  prdsinvlem  19178  rng1zrlem  20322  pws1  20471  rngcrescrhm  20852  frlmphl  22000  ovolunlem1  25731  0plef  25906  0pledm  25907  itg1ge0  25920  mbfi1fseqlem5  25953  itg2addlem  25992  qaa  26563  precsexlem1  28480  precsexlem2  28481  precsexlem3  28482  precsexlem4  28483  precsexlem5  28484  ex-fpar  30950  0vfval  31095  xrge0pluscn  34458  bnj927  35287  bnj535  35407  fullfunfnv  36533  neibastop2lem  36987  fnmptif  46102  fourierdlem42  46985  cjnpoly  47765  fcoreslem4  47962  upgrimwlklem1  48821  rngcrescrhmALTV  49203  isofval2  49966