Theorem fneq1i 6578

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

Syntax hints:   ↔ wb 206   = wceq 1541   Fn wfn 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-fun 6483  df-fn 6484

This theorem is referenced by:  fnunop  6597  mptfnf  6616  fnopabg  6618  f1oun  6782  f1oi  6801  f1osn  6803  ovid  7487  curry1  8034  curry2  8037  fsplitfpar  8048  frrlem11  8226  tfrlem10  8306  tfr1  8316  seqomlem2  8370  seqomlem3  8371  seqomlem4  8372  fnseqom  8374  unblem4  9179  r1fnon  9660  alephfnon  9956  alephfplem4  9998  alephfp  9999  cfsmolem  10161  infpssrlem3  10196  compssiso  10265  hsmexlem5  10321  axdclem2  10411  wunex2  10629  wuncval2  10638  om2uzrani  13859  om2uzf1oi  13860  uzrdglem  13864  uzrdgfni  13865  uzrdg0i  13866  hashkf  14239  dmaf  17956  cdaf  17957  prdsinvlem  18962  srg1zr  20134  pws1  20244  rngcrescrhm  20600  frlmphl  21719  ovolunlem1  25426  0plef  25601  0pledm  25602  itg1ge0  25615  mbfi1fseqlem5  25648  itg2addlem  25687  qaa  26259  precsexlem1  28146  precsexlem2  28147  precsexlem3  28148  precsexlem4  28149  precsexlem5  28150  ex-fpar  30440  0vfval  30584  xrge0pluscn  33951  bnj927  34779  bnj535  34900  fullfunfnv  35986  neibastop2lem  36400  fnmptif  45308  fourierdlem42  46193  cjnpoly  46926  fcoreslem4  47103  upgrimwlklem1  47934  rngcrescrhmALTV  48317  isofval2  49070