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

Theorem fneq1i 5531
Description: Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
fneq1i.1  |-  F  =  G
Assertion
Ref Expression
fneq1i  |-  ( F  Fn  A  <->  G  Fn  A )

Proof of Theorem fneq1i
StepHypRef Expression
1 fneq1i.1 . 2  |-  F  =  G
2 fneq1 5526 . 2  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
31, 2ax-mp 8 1  |-  ( F  Fn  A  <->  G  Fn  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1652    Fn wfn 5441
This theorem is referenced by:  fnunsn  5544  fnopabg  5560  f1oun  5686  f1oi  5705  f1osn  5707  ovid  6182  curry1  6430  curry2  6433  tfrlem10  6640  tfr1  6650  seqomlem2  6700  seqomlem3  6701  seqomlem4  6702  fnseqom  6704  abianfp  6708  unblem4  7354  r1fnon  7683  alephfnon  7936  alephfplem4  7978  alephfp  7979  cfsmolem  8140  infpssrlem3  8175  compssiso  8244  hsmexlem5  8300  axdclem2  8390  wunex2  8603  wuncval2  8612  om2uzrani  11282  om2uzf1oi  11283  uzrdglem  11287  uzrdgfni  11288  uzrdg0i  11289  hashkf  11610  dmaf  14194  cdaf  14195  prdsinvlem  14916  pws1  15712  ovolunlem1  19383  0plef  19554  0pledm  19555  itg1ge0  19568  itg1addlem4  19581  mbfi1fseqlem5  19601  itg2addlem  19640  qaa  20230  2trllemD  21547  eupap1  21688  ghgrp  21946  0vfval  22075  mptfnf  24063  xrge0pluscn  24316  wfrlem5  25527  wfrlem13  25535  frrlem5  25551  fullfunfnv  25756  neibastop2lem  26343  bnj927  29040  bnj535  29162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-fun 5448  df-fn 5449
  Copyright terms: Public domain W3C validator