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

Theorem elixp 7541
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 7538 . 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 986 . . 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 926 . 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 252 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 187    /\ wa 370    /\ w3a 982    e. wcel 1872   A.wral 2771   _Vcvv 3080    Fn wfn 5596   ` cfv 5601   X_cixp 7534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-iota 5565  df-fun 5603  df-fn 5604  df-fv 5609  df-ixp 7535
This theorem is referenced by:  elixpconst  7542  ixpin  7559  ixpiin  7560  resixpfo  7572  elixpsn  7573  boxriin  7576  boxcutc  7577  ixpfi2  7882  ixpiunwdom  8116  dfac9  8574  ac9  8921  ac9s  8931  konigthlem  9001  xpscf  15472  cofucl  15793  yonedalem3  16165  psrbaglefi  18596  ptpjpre1  20585  ptpjcn  20625  ptpjopn  20626  ptclsg  20629  dfac14  20632  pthaus  20652  xkopt  20669  ptcmplem2  21067  ptcmplem3  21068  ptcmplem4  21069  prdsbl  21505  prdsxmslem2  21543  eulerpartlemb  29210  ptpcon  29965  finixpnum  31895  ptrest  31904  poimirlem29  31934  poimirlem30  31935  inixp  32020  prdstotbnd  32091  hoicvr  38275  hoidmvlelem3  38324
  Copyright terms: Public domain W3C validator