Theorem fneq1i 6618

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

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-fun 6516  df-fn 6517

This theorem is referenced by:  fnunop  6637  mptfnf  6656  fnopabg  6658  f1oun  6822  f1oi  6841  f1osn  6843  ovid  7533  curry1  8086  curry2  8089  fsplitfpar  8100  frrlem11  8278  tfrlem10  8358  tfr1  8368  seqomlem2  8422  seqomlem3  8423  seqomlem4  8424  fnseqom  8426  unblem4  9249  r1fnon  9727  alephfnon  10025  alephfplem4  10067  alephfp  10068  cfsmolem  10230  infpssrlem3  10265  compssiso  10334  hsmexlem5  10390  axdclem2  10480  wunex2  10698  wuncval2  10707  om2uzrani  13924  om2uzf1oi  13925  uzrdglem  13929  uzrdgfni  13930  uzrdg0i  13931  hashkf  14304  dmaf  18018  cdaf  18019  prdsinvlem  18988  srg1zr  20131  pws1  20241  rngcrescrhm  20600  frlmphl  21697  ovolunlem1  25405  0plef  25580  0pledm  25581  itg1ge0  25594  mbfi1fseqlem5  25627  itg2addlem  25666  qaa  26238  precsexlem1  28116  precsexlem2  28117  precsexlem3  28118  precsexlem4  28119  precsexlem5  28120  ex-fpar  30398  0vfval  30542  xrge0pluscn  33937  bnj927  34766  bnj535  34887  fullfunfnv  35941  neibastop2lem  36355  fnmptif  45266  fourierdlem42  46154  fcoreslem4  47071  upgrimwlklem1  47901  rngcrescrhmALTV  48272  isofval2  49025