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

Theorem elixp 6823
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 6820 . 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 938 . . 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 884 . 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 240 1  |-  ( F  e.  X_ x  e.  A  B 
<->  ( F  Fn  A  /\  A. x  e.  A  ( F `  x )  e.  B ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    /\ w3a 934    e. wcel 1684   A.wral 2543   _Vcvv 2788    Fn wfn 5250   ` cfv 5255   X_cixp 6817
This theorem is referenced by:  elixpconst  6824  ixpin  6841  ixpiin  6842  resixpfo  6854  elixpsn  6855  boxriin  6858  boxcutc  6859  ixpfi2  7154  ixpiunwdom  7305  dfac9  7762  ac9  8110  ac9s  8120  konigthlem  8190  xpscf  13468  cofucl  13762  yonedalem3  14054  psrbaglefi  16118  ptpjpre1  17266  ptpjcn  17305  ptpjopn  17306  ptclsg  17309  dfac14  17312  pthaus  17332  xkopt  17349  ptcmplem2  17747  ptcmplem3  17748  ptcmplem4  17749  prdsbl  18037  prdsxmslem2  18075  ptpcon  23764  npincppr  25159  repcpwti  25161  cbicp  25166  inixp  26399  prdstotbnd  26518
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fn 5258  df-fv 5263  df-ixp 6818
  Copyright terms: Public domain W3C validator