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

Theorem elixp 7801
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 7798 . 2 (𝐹X𝑥𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
2 elixp.1 . . 3 𝐹 ∈ V
3 3anass 1035 . . 3 ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵)))
42, 3mpbiran 955 . 2 ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
51, 4bitri 263 1 (𝐹X𝑥𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383  w3a 1031  wcel 1977  wral 2896  Vcvv 3173   Fn wfn 5799  cfv 5804  Xcixp 7794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812  df-ixp 7795
This theorem is referenced by:  elixpconst  7802  ixpin  7819  ixpiin  7820  resixpfo  7832  elixpsn  7833  boxriin  7836  boxcutc  7837  ixpfi2  8147  ixpiunwdom  8379  dfac9  8841  ac9  9188  ac9s  9198  konigthlem  9269  xpscf  16049  cofucl  16371  yonedalem3  16743  psrbaglefi  19193  ptpjpre1  21184  ptpjcn  21224  ptpjopn  21225  ptclsg  21228  dfac14  21231  pthaus  21251  xkopt  21268  ptcmplem2  21667  ptcmplem3  21668  ptcmplem4  21669  prdsbl  22106  prdsxmslem2  22144  eulerpartlemb  29757  ptpcon  30469  finixpnum  32564  ptrest  32578  poimirlem29  32608  poimirlem30  32609  inixp  32693  prdstotbnd  32763  ioorrnopnlem  39200  hoicvr  39438  hoidmvlelem3  39487  hspdifhsp  39506  hspmbllem2  39517
  Copyright terms: Public domain W3C validator