MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fneq1i Structured version   Visualization version   GIF version

Theorem fneq1i 6443
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
StepHypRef Expression
1 fneq1i.1 . 2 𝐹 = 𝐺
2 fneq1 6437 . 2 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
31, 2ax-mp 5 1 (𝐹 Fn 𝐴𝐺 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528   Fn wfn 6343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-br 5058  df-opab 5120  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-fun 6350  df-fn 6351
This theorem is referenced by:  fnunsn  6457  mptfnf  6476  fnopabg  6478  f1oun  6627  f1oi  6645  f1osn  6647  ovid  7280  curry1  7788  curry2  7791  fsplitfpar  7803  wfrlem5  7948  wfrlem13  7956  tfrlem10  8012  tfr1  8022  seqomlem2  8076  seqomlem3  8077  seqomlem4  8078  fnseqom  8080  unblem4  8761  r1fnon  9184  alephfnon  9479  alephfplem4  9521  alephfp  9522  cfsmolem  9680  infpssrlem3  9715  compssiso  9784  hsmexlem5  9840  axdclem2  9930  wunex2  10148  wuncval2  10157  om2uzrani  13308  om2uzf1oi  13309  uzrdglem  13313  uzrdgfni  13314  uzrdg0i  13315  hashkf  13680  dmaf  17297  cdaf  17298  prdsinvlem  18146  srg1zr  19208  pws1  19295  frlmphl  20853  ovolunlem1  24025  0plef  24200  0pledm  24201  itg1ge0  24214  itg1addlem4  24227  mbfi1fseqlem5  24247  itg2addlem  24286  qaa  24839  ex-fpar  28168  0vfval  28310  xrge0pluscn  31082  bnj927  31939  bnj535  32061  frrlem11  33030  fullfunfnv  33304  neibastop2lem  33605  fourierdlem42  42311  rngcrescrhm  44284  rngcrescrhmALTV  44302
  Copyright terms: Public domain W3C validator