Theorem fneq1i 6637

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   Fn wfn 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-fun 6541  df-fn 6542

This theorem is used by:  fnunop  6656  mptfnf  6675  fnopabg  6677  f1oun  6845  f1oiOLD  6865  f1osn  6867  ovid  7562  curry1  8118  curry2  8121  fsplitfpar  8132  frrlem11  8318  tfrlem10  8399  tfr1  8409  seqomlem2  8465  seqomlem3  8466  seqomlem4  8467  fnseqom  8469  unblem4  9291  r1fnon  9777  alephfnon  10148  alephfplem4  10190  alephfp  10191  cfsmolem  10352  infpssrlem3  10387  compssiso  10456  hsmexlem5  10512  axdclem2  10602  wunex2  10827  wuncval2  10836  om2uzrani  14099  om2uzf1oi  14100  uzrdglem  14104  uzrdgfni  14105  uzrdg0i  14106  hashkf  14480  dmaf  18230  cdaf  18231  prdsinvlem  19265  rng1zrlem  20409  pws1  20560  rngcrescrhm  20942  frlmphl  22093  ovolunlem1  25824  0plef  25999  0pledm  26000  itg1ge0  26013  mbfi1fseqlem5  26046  itg2addlem  26085  qaa  26653  precsexlem1  28599  precsexlem2  28600  precsexlem3  28601  precsexlem4  28602  precsexlem5  28603  ex-fpar  31069  0vfval  31214  xrge0pluscn  34619  bnj927  35447  bnj535  35567  fullfunfnv  36803  neibastop2lem  37241  fnmptif  46371  fourierdlem42  47253  cjnpoly  48033  fcoreslem4  48230  upgrimwlklem1  49089  rngcrescrhmALTV  49471  isofval2  50240