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

Theorem elixp 7275
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 7272 . 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 969 . . 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 909 . 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 249 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 184    /\ wa 369    /\ w3a 965    e. wcel 1756   A.wral 2720   _Vcvv 2977    Fn wfn 5418   ` cfv 5423   X_cixp 7268
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-iota 5386  df-fun 5425  df-fn 5426  df-fv 5431  df-ixp 7269
This theorem is referenced by:  elixpconst  7276  ixpin  7293  ixpiin  7294  resixpfo  7306  elixpsn  7307  boxriin  7310  boxcutc  7311  ixpfi2  7614  ixpiunwdom  7811  dfac9  8310  ac9  8657  ac9s  8667  konigthlem  8737  xpscf  14509  cofucl  14803  yonedalem3  15095  psrbaglefi  17446  psrbaglefiOLD  17447  ptpjpre1  19149  ptpjcn  19189  ptpjopn  19190  ptclsg  19193  dfac14  19196  pthaus  19216  xkopt  19233  ptcmplem2  19630  ptcmplem3  19631  ptcmplem4  19632  prdsbl  20071  prdsxmslem2  20109  eulerpartlemb  26756  ptpcon  27127  finixpnum  28419  ptrest  28430  inixp  28627  prdstotbnd  28698
  Copyright terms: Public domain W3C validator