Theorem fneq1i 6530

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

Syntax hints:   ↔ wb 205   = wceq 1539   Fn wfn 6428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-fun 6435  df-fn 6436

This theorem is referenced by:  fnunop  6547  mptfnf  6568  fnopabg  6570  f1oun  6735  f1oi  6754  f1osn  6756  ovid  7414  curry1  7944  curry2  7947  fsplitfpar  7959  frrlem11  8112  wfrlem5OLD  8144  wfrlem13OLD  8152  tfrlem10  8218  tfr1  8228  seqomlem2  8282  seqomlem3  8283  seqomlem4  8284  fnseqom  8286  unblem4  9069  r1fnon  9525  alephfnon  9821  alephfplem4  9863  alephfp  9864  cfsmolem  10026  infpssrlem3  10061  compssiso  10130  hsmexlem5  10186  axdclem2  10276  wunex2  10494  wuncval2  10503  om2uzrani  13672  om2uzf1oi  13673  uzrdglem  13677  uzrdgfni  13678  uzrdg0i  13679  hashkf  14046  dmaf  17764  cdaf  17765  prdsinvlem  18684  srg1zr  19765  pws1  19855  frlmphl  20988  ovolunlem1  24661  0plef  24836  0pledm  24837  itg1ge0  24850  itg1addlem4OLD  24864  mbfi1fseqlem5  24884  itg2addlem  24923  qaa  25483  ex-fpar  28826  0vfval  28968  xrge0pluscn  31890  bnj927  32749  bnj535  32870  fullfunfnv  34248  neibastop2lem  34549  fourierdlem42  43690  fcoreslem4  44560  rngcrescrhm  45643  rngcrescrhmALTV  45661