Theorem fneq1i 6661

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   Fn wfn 6556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-fun 6563  df-fn 6564

This theorem is used by:  fnunop  6680  mptfnf  6699  fnopabg  6701  f1oun  6869  f1oiOLD  6890  f1osn  6892  ovid  7588  curry1  8145  curry2  8148  fsplitfpar  8159  frrlem11  8345  tfrlem10  8426  tfr1  8436  seqomlem2  8492  seqomlem3  8493  seqomlem4  8494  fnseqom  8496  unblem4  9318  r1fnon  9803  alephfnon  10174  alephfplem4  10216  alephfp  10217  cfsmolem  10378  infpssrlem3  10413  compssiso  10482  hsmexlem5  10538  axdclem2  10628  wunex2  10853  wuncval2  10862  om2uzrani  14125  om2uzf1oi  14126  uzrdglem  14130  uzrdgfni  14131  uzrdg0i  14132  hashkf  14506  dmaf  18256  cdaf  18257  prdsinvlem  19291  rng1zrlem  20436  pws1  20587  rngcrescrhm  20969  frlmphl  22120  ovolunlem1  25851  0plef  26026  0pledm  26027  itg1ge0  26040  mbfi1fseqlem5  26073  itg2addlem  26112  qaa  26680  precsexlem1  28626  precsexlem2  28627  precsexlem3  28628  precsexlem4  28629  precsexlem5  28630  ex-fpar  31096  0vfval  31241  xrge0pluscn  34655  bnj927  35483  bnj535  35603  fullfunfnv  36901  neibastop2lem  37339  fnmptif  46492  fourierdlem42  47374  cjnpoly  48154  fcoreslem4  48351  upgrimwlklem1  49210  rngcrescrhmALTV  49592  isofval2  50361