Theorem fneq1i 6639

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

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

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-fun 6545  df-fn 6546

This theorem is used by:  fnunop  6658  mptfnf  6677  fnopabg  6679  f1oun  6847  f1oiOLD  6867  f1osn  6869  ovid  7564  curry1  8108  curry2  8111  fsplitfpar  8122  frrlem11  8302  tfrlem10  8383  tfr1  8393  seqomlem2  8447  seqomlem3  8448  seqomlem4  8449  fnseqom  8451  unblem4  9265  r1fnon  9749  alephfnon  10068  alephfplem4  10110  alephfp  10111  cfsmolem  10272  infpssrlem3  10307  compssiso  10376  hsmexlem5  10432  axdclem2  10522  wunex2  10741  wuncval2  10750  om2uzrani  14008  om2uzf1oi  14009  uzrdglem  14013  uzrdgfni  14014  uzrdg0i  14015  hashkf  14388  dmaf  18131  cdaf  18132  prdsinvlem  19146  rng1zrlem  20290  pws1  20439  rngcrescrhm  20820  frlmphl  21968  ovolunlem1  25693  0plef  25868  0pledm  25869  itg1ge0  25882  mbfi1fseqlem5  25915  itg2addlem  25954  qaa  26521  precsexlem1  28437  precsexlem2  28438  precsexlem3  28439  precsexlem4  28440  precsexlem5  28441  ex-fpar  30850  0vfval  30995  xrge0pluscn  34361  bnj927  35190  bnj535  35310  fullfunfnv  36459  neibastop2lem  36912  fnmptif  46021  fourierdlem42  46904  cjnpoly  47667  fcoreslem4  47844  upgrimwlklem1  48703  rngcrescrhmALTV  49086  isofval2  49851