Theorem fneq1i 6666

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

Syntax hints:   ↔ wb 206   = wceq 1537   Fn wfn 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-fun 6565  df-fn 6566

This theorem is referenced by:  fnunop  6685  mptfnf  6704  fnopabg  6706  f1oun  6868  f1oi  6887  f1osn  6889  ovid  7574  curry1  8128  curry2  8131  fsplitfpar  8142  frrlem11  8320  wfrlem5OLD  8352  wfrlem13OLD  8360  tfrlem10  8426  tfr1  8436  seqomlem2  8490  seqomlem3  8491  seqomlem4  8492  fnseqom  8494  unblem4  9329  r1fnon  9805  alephfnon  10103  alephfplem4  10145  alephfp  10146  cfsmolem  10308  infpssrlem3  10343  compssiso  10412  hsmexlem5  10468  axdclem2  10558  wunex2  10776  wuncval2  10785  om2uzrani  13990  om2uzf1oi  13991  uzrdglem  13995  uzrdgfni  13996  uzrdg0i  13997  hashkf  14368  dmaf  18103  cdaf  18104  prdsinvlem  19080  srg1zr  20233  pws1  20339  rngcrescrhm  20701  frlmphl  21819  ovolunlem1  25546  0plef  25721  0pledm  25722  itg1ge0  25735  itg1addlem4OLD  25749  mbfi1fseqlem5  25769  itg2addlem  25808  qaa  26380  precsexlem1  28246  precsexlem2  28247  precsexlem3  28248  precsexlem4  28249  precsexlem5  28250  ex-fpar  30491  0vfval  30635  xrge0pluscn  33901  bnj927  34762  bnj535  34883  fullfunfnv  35928  neibastop2lem  36343  fnmptif  45211  fourierdlem42  46105  fcoreslem4  47016  rngcrescrhmALTV  48124