Theorem fneq1i 6420

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

Syntax hints:   ↔ wb 209   = wceq 1538   Fn wfn 6319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-fun 6326  df-fn 6327

This theorem is referenced by:  fnunsn  6436  mptfnf  6455  fnopabg  6457  f1oun  6609  f1oi  6627  f1osn  6629  ovid  7270  curry1  7782  curry2  7785  fsplitfpar  7797  wfrlem5  7942  wfrlem13  7950  tfrlem10  8006  tfr1  8016  seqomlem2  8070  seqomlem3  8071  seqomlem4  8072  fnseqom  8074  unblem4  8757  r1fnon  9180  alephfnon  9476  alephfplem4  9518  alephfp  9519  cfsmolem  9681  infpssrlem3  9716  compssiso  9785  hsmexlem5  9841  axdclem2  9931  wunex2  10149  wuncval2  10158  om2uzrani  13315  om2uzf1oi  13316  uzrdglem  13320  uzrdgfni  13321  uzrdg0i  13322  hashkf  13688  dmaf  17301  cdaf  17302  prdsinvlem  18200  srg1zr  19272  pws1  19362  frlmphl  20470  ovolunlem1  24101  0plef  24276  0pledm  24277  itg1ge0  24290  itg1addlem4  24303  mbfi1fseqlem5  24323  itg2addlem  24362  qaa  24919  ex-fpar  28247  0vfval  28389  xrge0pluscn  31293  bnj927  32150  bnj535  32272  frrlem11  33246  fullfunfnv  33520  neibastop2lem  33821  fourierdlem42  42791  rngcrescrhm  44709  rngcrescrhmALTV  44727