Theorem fneq1i 6589

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

Syntax hints:   ↔ wb 207   = wceq 1547   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-fun 6494  df-fn 6495

This theorem is referenced by:  fnunop  6608  mptfnf  6627  fnopabg  6629  f1oun  6793  f1oiOLD  6813  f1osn  6815  ovid  7504  curry1  8050  curry2  8053  fsplitfpar  8064  frrlem11  8243  tfrlem10  8323  tfr1  8333  seqomlem2  8387  seqomlem3  8388  seqomlem4  8389  fnseqom  8391  unblem4  9202  r1fnon  9689  alephfnon  9985  alephfplem4  10027  alephfp  10028  cfsmolem  10190  infpssrlem3  10225  compssiso  10294  hsmexlem5  10350  axdclem2  10440  wunex2  10659  wuncval2  10668  om2uzrani  13912  om2uzf1oi  13913  uzrdglem  13917  uzrdgfni  13918  uzrdg0i  13919  hashkf  14292  dmaf  18014  cdaf  18015  prdsinvlem  19023  srg1zr  20194  pws1  20302  rngcrescrhm  20663  frlmphl  21763  ovolunlem1  25489  0plef  25664  0pledm  25665  itg1ge0  25678  mbfi1fseqlem5  25711  itg2addlem  25750  qaa  26314  precsexlem1  28224  precsexlem2  28225  precsexlem3  28226  precsexlem4  28227  precsexlem5  28228  ex-fpar  30557  0vfval  30702  xrge0pluscn  34131  bnj927  34959  bnj535  35079  fullfunfnv  36181  neibastop2lem  36595  fnmptif  45716  fourierdlem42  46599  cjnpoly  47359  fcoreslem4  47536  upgrimwlklem1  48395  rngcrescrhmALTV  48778  isofval2  49529