Theorem fneq1i 6583

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

Syntax hints:   ↔ wb 206   = wceq 1541   Fn wfn 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-fun 6488  df-fn 6489

This theorem is referenced by:  fnunop  6602  mptfnf  6621  fnopabg  6623  f1oun  6787  f1oiOLD  6807  f1osn  6809  ovid  7493  curry1  8040  curry2  8043  fsplitfpar  8054  frrlem11  8232  tfrlem10  8312  tfr1  8322  seqomlem2  8376  seqomlem3  8377  seqomlem4  8378  fnseqom  8380  unblem4  9186  r1fnon  9667  alephfnon  9963  alephfplem4  10005  alephfp  10006  cfsmolem  10168  infpssrlem3  10203  compssiso  10272  hsmexlem5  10328  axdclem2  10418  wunex2  10636  wuncval2  10645  om2uzrani  13861  om2uzf1oi  13862  uzrdglem  13866  uzrdgfni  13867  uzrdg0i  13868  hashkf  14241  dmaf  17958  cdaf  17959  prdsinvlem  18964  srg1zr  20135  pws1  20245  rngcrescrhm  20601  frlmphl  21720  ovolunlem1  25426  0plef  25601  0pledm  25602  itg1ge0  25615  mbfi1fseqlem5  25648  itg2addlem  25687  qaa  26259  precsexlem1  28146  precsexlem2  28147  precsexlem3  28148  precsexlem4  28149  precsexlem5  28150  ex-fpar  30444  0vfval  30588  xrge0pluscn  33974  bnj927  34802  bnj535  34923  fullfunfnv  36011  neibastop2lem  36425  fnmptif  45386  fourierdlem42  46271  cjnpoly  47013  fcoreslem4  47190  upgrimwlklem1  48021  rngcrescrhmALTV  48404  isofval2  49157