Theorem fneq1i 6612

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

Syntax hints:   ↔ wb 208   = wceq 1559   Fn wfn 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-fun 6517  df-fn 6518

This theorem is referenced by:  fnunop  6631  mptfnf  6650  fnopabg  6652  f1oun  6820  f1oiOLD  6840  f1osn  6842  ovid  7531  curry1  8076  curry2  8079  fsplitfpar  8090  frrlem11  8270  tfrlem10  8351  tfr1  8361  seqomlem2  8415  seqomlem3  8416  seqomlem4  8417  fnseqom  8419  unblem4  9232  r1fnon  9718  alephfnon  10014  alephfplem4  10056  alephfp  10057  cfsmolem  10220  infpssrlem3  10255  compssiso  10324  hsmexlem5  10380  axdclem2  10470  wunex2  10689  wuncval2  10698  om2uzrani  13958  om2uzf1oi  13959  uzrdglem  13963  uzrdgfni  13964  uzrdg0i  13965  hashkf  14338  dmaf  18072  cdaf  18073  prdsinvlem  19081  srg1zr  20251  pws1  20359  rngcrescrhm  20720  frlmphl  21820  ovolunlem1  25546  0plef  25721  0pledm  25722  itg1ge0  25735  mbfi1fseqlem5  25768  itg2addlem  25807  qaa  26374  precsexlem1  28287  precsexlem2  28288  precsexlem3  28289  precsexlem4  28290  precsexlem5  28291  ex-fpar  30620  0vfval  30765  xrge0pluscn  34197  bnj927  35025  bnj535  35145  fullfunfnv  36256  neibastop2lem  36680  fnmptif  45800  fourierdlem42  46683  cjnpoly  47443  fcoreslem4  47620  upgrimwlklem1  48479  rngcrescrhmALTV  48862  isofval2  49613