Theorem fneq1i 6615

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-fun 6513  df-fn 6514

This theorem is referenced by:  fnunop  6634  mptfnf  6653  fnopabg  6655  f1oun  6819  f1oi  6838  f1osn  6840  ovid  7530  curry1  8083  curry2  8086  fsplitfpar  8097  frrlem11  8275  tfrlem10  8355  tfr1  8365  seqomlem2  8419  seqomlem3  8420  seqomlem4  8421  fnseqom  8423  unblem4  9242  r1fnon  9720  alephfnon  10018  alephfplem4  10060  alephfp  10061  cfsmolem  10223  infpssrlem3  10258  compssiso  10327  hsmexlem5  10383  axdclem2  10473  wunex2  10691  wuncval2  10700  om2uzrani  13917  om2uzf1oi  13918  uzrdglem  13922  uzrdgfni  13923  uzrdg0i  13924  hashkf  14297  dmaf  18011  cdaf  18012  prdsinvlem  18981  srg1zr  20124  pws1  20234  rngcrescrhm  20593  frlmphl  21690  ovolunlem1  25398  0plef  25573  0pledm  25574  itg1ge0  25587  mbfi1fseqlem5  25620  itg2addlem  25659  qaa  26231  precsexlem1  28109  precsexlem2  28110  precsexlem3  28111  precsexlem4  28112  precsexlem5  28113  ex-fpar  30391  0vfval  30535  xrge0pluscn  33930  bnj927  34759  bnj535  34880  fullfunfnv  35934  neibastop2lem  36348  fnmptif  45259  fourierdlem42  46147  cjnpoly  46890  fcoreslem4  47067  upgrimwlklem1  47897  rngcrescrhmALTV  48268  isofval2  49021