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

Theorem fneq1i 6125
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 6119 . 2 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
31, 2ax-mp 5 1 (𝐹 Fn 𝐴𝐺 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1631   Fn wfn 6026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-br 4787  df-opab 4847  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-fun 6033  df-fn 6034
This theorem is referenced by:  fnunsn  6138  mptfnf  6155  fnopabg  6157  f1oun  6297  f1oi  6315  f1osn  6317  ovid  6924  curry1  7420  curry2  7423  wfrlem5  7572  wfrlem13  7580  tfrlem10  7636  tfr1  7646  seqomlem2  7699  seqomlem3  7700  seqomlem4  7701  fnseqom  7703  unblem4  8371  r1fnon  8794  alephfnon  9088  alephfplem4  9130  alephfp  9131  cfsmolem  9294  infpssrlem3  9329  compssiso  9398  hsmexlem5  9454  axdclem2  9544  wunex2  9762  wuncval2  9771  om2uzrani  12959  om2uzf1oi  12960  uzrdglem  12964  uzrdgfni  12965  uzrdg0i  12966  hashkf  13323  dmaf  16906  cdaf  16907  prdsinvlem  17732  srg1zr  18737  pws1  18824  frlmphl  20337  ovolunlem1  23485  0plef  23659  0pledm  23660  itg1ge0  23673  itg1addlem4  23686  mbfi1fseqlem5  23706  itg2addlem  23745  qaa  24298  0vfval  27801  xrge0pluscn  30326  bnj927  31177  bnj535  31298  frrlem5  32121  fullfunfnv  32390  neibastop2lem  32692  fourierdlem42  40883  rngcrescrhm  42613  rngcrescrhmALTV  42631
  Copyright terms: Public domain W3C validator