Theorem fneq1i 6589

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-fun 6494  df-fn 6495

This theorem is referenced by:  fnunop  6608  mptfnf  6627  fnopabg  6629  f1oun  6793  f1oiOLD  6813  f1osn  6815  ovid  7499  curry1  8046  curry2  8049  fsplitfpar  8060  frrlem11  8238  tfrlem10  8318  tfr1  8328  seqomlem2  8382  seqomlem3  8383  seqomlem4  8384  fnseqom  8386  unblem4  9195  r1fnon  9679  alephfnon  9975  alephfplem4  10017  alephfp  10018  cfsmolem  10180  infpssrlem3  10215  compssiso  10284  hsmexlem5  10340  axdclem2  10430  wunex2  10649  wuncval2  10658  om2uzrani  13875  om2uzf1oi  13876  uzrdglem  13880  uzrdgfni  13881  uzrdg0i  13882  hashkf  14255  dmaf  17973  cdaf  17974  prdsinvlem  18979  srg1zr  20150  pws1  20260  rngcrescrhm  20617  frlmphl  21736  ovolunlem1  25454  0plef  25629  0pledm  25630  itg1ge0  25643  mbfi1fseqlem5  25676  itg2addlem  25715  qaa  26287  precsexlem1  28203  precsexlem2  28204  precsexlem3  28205  precsexlem4  28206  precsexlem5  28207  ex-fpar  30537  0vfval  30681  xrge0pluscn  34097  bnj927  34925  bnj535  35046  fullfunfnv  36140  neibastop2lem  36554  fnmptif  45509  fourierdlem42  46393  cjnpoly  47135  fcoreslem4  47312  upgrimwlklem1  48143  rngcrescrhmALTV  48526  isofval2  49277