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

Theorem fneq1i 5973
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 5967 . 2 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
31, 2ax-mp 5 1 (𝐹 Fn 𝐴𝐺 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1481   Fn wfn 5871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-fun 5878  df-fn 5879
This theorem is referenced by:  fnunsn  5986  mptfnf  6002  fnopabg  6004  f1oun  6143  f1oi  6161  f1osn  6163  ovid  6762  curry1  7254  curry2  7257  wfrlem5  7404  wfrlem13  7412  tfrlem10  7468  tfr1  7478  seqomlem2  7531  seqomlem3  7532  seqomlem4  7533  fnseqom  7535  unblem4  8200  r1fnon  8615  alephfnon  8873  alephfplem4  8915  alephfp  8916  cfsmolem  9077  infpssrlem3  9112  compssiso  9181  hsmexlem5  9237  axdclem2  9327  wunex2  9545  wuncval2  9554  om2uzrani  12734  om2uzf1oi  12735  uzrdglem  12739  uzrdgfni  12740  uzrdg0i  12741  hashkf  13102  dmaf  16680  cdaf  16681  prdsinvlem  17505  srg1zr  18510  pws1  18597  frlmphl  20101  ovolunlem1  23246  0plef  23420  0pledm  23421  itg1ge0  23434  itg1addlem4  23447  mbfi1fseqlem5  23467  itg2addlem  23506  qaa  24059  0vfval  27431  xrge0pluscn  29960  bnj927  30813  bnj535  30934  frrlem5  31758  fullfunfnv  32028  neibastop2lem  32330  fourierdlem42  40129  rngcrescrhm  41850  rngcrescrhmALTV  41868
  Copyright terms: Public domain W3C validator