Theorem fneq1i 5985

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

Syntax hints:   ↔ wb 196   = wceq 1483   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-fun 5890  df-fn 5891

This theorem is referenced by:  fnunsn  5998  mptfnf  6015  fnopabg  6017  f1oun  6156  f1oi  6174  f1osn  6176  ovid  6777  curry1  7269  curry2  7272  wfrlem5  7419  wfrlem13  7427  tfrlem10  7483  tfr1  7493  seqomlem2  7546  seqomlem3  7547  seqomlem4  7548  fnseqom  7550  unblem4  8215  r1fnon  8630  alephfnon  8888  alephfplem4  8930  alephfp  8931  cfsmolem  9092  infpssrlem3  9127  compssiso  9196  hsmexlem5  9252  axdclem2  9342  wunex2  9560  wuncval2  9569  om2uzrani  12751  om2uzf1oi  12752  uzrdglem  12756  uzrdgfni  12757  uzrdg0i  12758  hashkf  13119  dmaf  16699  cdaf  16700  prdsinvlem  17524  srg1zr  18529  pws1  18616  frlmphl  20120  ovolunlem1  23265  0plef  23439  0pledm  23440  itg1ge0  23453  itg1addlem4  23466  mbfi1fseqlem5  23486  itg2addlem  23525  qaa  24078  0vfval  27461  xrge0pluscn  29986  bnj927  30839  bnj535  30960  frrlem5  31784  fullfunfnv  32053  neibastop2lem  32355  fourierdlem42  40366  rngcrescrhm  42085  rngcrescrhmALTV  42103