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

Theorem elixp 8609
Description: Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.)
Hypothesis
Ref Expression
elixp.1 𝐹 ∈ V
Assertion
Ref Expression
elixp (𝐹X𝑥𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
Distinct variable groups:   𝑥,𝐹   𝑥,𝐴
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem elixp
StepHypRef Expression
1 elixp2 8606 . 2 (𝐹X𝑥𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
2 elixp.1 . . 3 𝐹 ∈ V
3 3anass 1097 . . 3 ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵)))
42, 3mpbiran 709 . 2 ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
51, 4bitri 278 1 (𝐹X𝑥𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  w3a 1089  wcel 2112  wral 3064  Vcvv 3423   Fn wfn 6396  cfv 6401  Xcixp 8602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-ral 3069  df-rab 3073  df-v 3425  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-iota 6359  df-fun 6403  df-fn 6404  df-fv 6409  df-ixp 8603
This theorem is referenced by:  elixpconst  8610  ixpin  8628  ixpiin  8629  resixpfo  8641  elixpsn  8642  boxriin  8645  boxcutc  8646  ixpfi2  9004  ixpiunwdom  9236  dfac9  9780  ac9  10127  ac9s  10137  konigthlem  10212  cofucl  17427  yonedalem3  17821  psrbaglefi  20923  psrbaglefiOLD  20924  ptpjpre1  22500  ptpjcn  22540  ptpjopn  22541  ptclsg  22544  dfac14  22547  pthaus  22567  xkopt  22584  ptcmplem2  22982  ptcmplem3  22983  ptcmplem4  22984  prdsbl  23421  prdsxmslem2  23459  eulerpartlemb  32079  ptpconn  32939  finixpnum  35536  ptrest  35550  poimirlem29  35580  poimirlem30  35581  inixp  35660  prdstotbnd  35726  ioorrnopnlem  43566  hoicvr  43807  hoidmvlelem3  43856  hspdifhsp  43875  hspmbllem2  43886
  Copyright terms: Public domain W3C validator