Theorem fneq1i 6585

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

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

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 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-fun 6490  df-fn 6491

This theorem is referenced by:  fnunop  6604  mptfnf  6623  fnopabg  6625  f1oun  6789  f1oiOLD  6809  f1osn  6811  ovid  7495  curry1  8042  curry2  8045  fsplitfpar  8056  frrlem11  8234  tfrlem10  8314  tfr1  8324  seqomlem2  8378  seqomlem3  8379  seqomlem4  8380  fnseqom  8382  unblem4  9188  r1fnon  9669  alephfnon  9965  alephfplem4  10007  alephfp  10008  cfsmolem  10170  infpssrlem3  10205  compssiso  10274  hsmexlem5  10330  axdclem2  10420  wunex2  10638  wuncval2  10647  om2uzrani  13863  om2uzf1oi  13864  uzrdglem  13868  uzrdgfni  13869  uzrdg0i  13870  hashkf  14243  dmaf  17960  cdaf  17961  prdsinvlem  18966  srg1zr  20137  pws1  20247  rngcrescrhm  20603  frlmphl  21722  ovolunlem1  25428  0plef  25603  0pledm  25604  itg1ge0  25617  mbfi1fseqlem5  25650  itg2addlem  25689  qaa  26261  precsexlem1  28148  precsexlem2  28149  precsexlem3  28150  precsexlem4  28151  precsexlem5  28152  ex-fpar  30446  0vfval  30590  xrge0pluscn  33976  bnj927  34804  bnj535  34925  fullfunfnv  36013  neibastop2lem  36427  fnmptif  45389  fourierdlem42  46274  cjnpoly  47016  fcoreslem4  47193  upgrimwlklem1  48024  rngcrescrhmALTV  48407  isofval2  49160