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

Theorem elixp 7560
Description: Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.)
Hypothesis
Ref Expression
elixp.1  |-  F  e. 
_V
Assertion
Ref Expression
elixp  |-  ( F  e.  X_ x  e.  A  B 
<->  ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B ) )
Distinct variable groups:    x, F    x, A
Allowed substitution hint:    B( x)

Proof of Theorem elixp
StepHypRef Expression
1 elixp2 7557 . 2  |-  ( F  e.  X_ x  e.  A  B 
<->  ( F  e.  _V  /\  F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B ) )
2 elixp.1 . . 3  |-  F  e. 
_V
3 3anass 995 . . 3  |-  ( ( F  e.  _V  /\  F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  <->  ( F  e.  _V  /\  ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B ) ) )
42, 3mpbiran 934 . 2  |-  ( ( F  e.  _V  /\  F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B )  <->  ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B
) )
51, 4bitri 257 1  |-  ( F  e.  X_ x  e.  A  B 
<->  ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375    /\ w3a 991    e. wcel 1898   A.wral 2749   _Vcvv 3057    Fn wfn 5600   ` cfv 5605   X_cixp 7553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-iota 5569  df-fun 5607  df-fn 5608  df-fv 5613  df-ixp 7554
This theorem is referenced by:  elixpconst  7561  ixpin  7578  ixpiin  7579  resixpfo  7591  elixpsn  7592  boxriin  7595  boxcutc  7596  ixpfi2  7903  ixpiunwdom  8137  dfac9  8597  ac9  8944  ac9s  8954  konigthlem  9024  xpscf  15527  cofucl  15848  yonedalem3  16220  psrbaglefi  18651  ptpjpre1  20641  ptpjcn  20681  ptpjopn  20682  ptclsg  20685  dfac14  20688  pthaus  20708  xkopt  20725  ptcmplem2  21123  ptcmplem3  21124  ptcmplem4  21125  prdsbl  21561  prdsxmslem2  21599  eulerpartlemb  29251  ptpcon  30006  finixpnum  31976  ptrest  31985  poimirlem29  32015  poimirlem30  32016  inixp  32101  prdstotbnd  32172  hoicvr  38477  hoidmvlelem3  38526  hspdifhsp  38545  hspmbllem2  38556
  Copyright terms: Public domain W3C validator