Theorem fneq1i 6583

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

Syntax hints:   ↔ wb 206   = wceq 1540   Fn wfn 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-fun 6488  df-fn 6489

This theorem is referenced by:  fnunop  6602  mptfnf  6621  fnopabg  6623  f1oun  6787  f1oi  6806  f1osn  6808  ovid  7494  curry1  8044  curry2  8047  fsplitfpar  8058  frrlem11  8236  tfrlem10  8316  tfr1  8326  seqomlem2  8380  seqomlem3  8381  seqomlem4  8382  fnseqom  8384  unblem4  9200  r1fnon  9682  alephfnon  9978  alephfplem4  10020  alephfp  10021  cfsmolem  10183  infpssrlem3  10218  compssiso  10287  hsmexlem5  10343  axdclem2  10433  wunex2  10651  wuncval2  10660  om2uzrani  13877  om2uzf1oi  13878  uzrdglem  13882  uzrdgfni  13883  uzrdg0i  13884  hashkf  14257  dmaf  17974  cdaf  17975  prdsinvlem  18946  srg1zr  20118  pws1  20228  rngcrescrhm  20587  frlmphl  21706  ovolunlem1  25414  0plef  25589  0pledm  25590  itg1ge0  25603  mbfi1fseqlem5  25636  itg2addlem  25675  qaa  26247  precsexlem1  28132  precsexlem2  28133  precsexlem3  28134  precsexlem4  28135  precsexlem5  28136  ex-fpar  30424  0vfval  30568  xrge0pluscn  33909  bnj927  34738  bnj535  34859  fullfunfnv  35922  neibastop2lem  36336  fnmptif  45246  fourierdlem42  46134  cjnpoly  46877  fcoreslem4  47054  upgrimwlklem1  47885  rngcrescrhmALTV  48268  isofval2  49021