Theorem fneq1i 6628

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-fun 6533  df-fn 6534

This theorem is used by:  fnunop  6647  mptfnf  6666  fnopabg  6668  f1oun  6836  f1oiOLD  6856  f1osn  6858  ovid  7553  curry1  8104  curry2  8107  fsplitfpar  8118  frrlem11  8298  tfrlem10  8379  tfr1  8389  seqomlem2  8445  seqomlem3  8446  seqomlem4  8447  fnseqom  8449  unblem4  9271  r1fnon  9757  alephfnon  10125  alephfplem4  10167  alephfp  10168  cfsmolem  10329  infpssrlem3  10364  compssiso  10433  hsmexlem5  10489  axdclem2  10579  wunex2  10804  wuncval2  10813  om2uzrani  14075  om2uzf1oi  14076  uzrdglem  14080  uzrdgfni  14081  uzrdg0i  14082  hashkf  14456  dmaf  18204  cdaf  18205  prdsinvlem  19239  rng1zrlem  20383  pws1  20534  rngcrescrhm  20916  frlmphl  22067  ovolunlem1  25798  0plef  25973  0pledm  25974  itg1ge0  25987  mbfi1fseqlem5  26020  itg2addlem  26059  qaa  26629  precsexlem1  28575  precsexlem2  28576  precsexlem3  28577  precsexlem4  28578  precsexlem5  28579  ex-fpar  31045  0vfval  31190  xrge0pluscn  34554  bnj927  35383  bnj535  35503  fullfunfnv  36680  neibastop2lem  37118  fnmptif  46220  fourierdlem42  47103  cjnpoly  47883  fcoreslem4  48080  upgrimwlklem1  48939  rngcrescrhmALTV  49321  isofval2  50084