Theorem elixp 8890

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

Step	Hyp	Ref	Expression
1		elixp2 8887	. 2 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
2		elixp.1	. . 3 ⊢ 𝐹 ∈ V
3		3anass 1109	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)))
4	2, 3	mpbiran 721	. 2 ⊢ ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5	1, 4	bitri 278	1 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   ∈ wcel 2145  ∀wral 3079  Vcvv 3457   Fn wfn 6520  ‘cfv 6525  Xcixp 8883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-opab 5168  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-iota 6481  df-fun 6527  df-fn 6528  df-fv 6533  df-ixp 8884

This theorem is referenced by:  elixpconst  8891  ixpin  8909  ixpiin  8910  resixpfo  8922  elixpsn  8923  boxriin  8926  boxcutc  8927  ixpfi2  9295  ixpiunwdom  9540  dfac9  10108  ac9  10455  ac9s  10465  konigthlem  10541  cofucl  17935  yonedalem3  18326  psrbaglefi  22036  ptpjpre1  23689  ptpjcn  23729  ptpjopn  23730  ptclsg  23733  dfac14  23736  pthaus  23756  xkopt  23773  ptcmplem2  24171  ptcmplem3  24172  ptcmplem4  24173  prdsbl  24609  prdsxmslem2  24647  eulerpartlemb  34675  ptpconn  35596  finixpnum  38116  ptrest  38130  poimirlem29  38160  poimirlem30  38161  inixp  38239  prdstotbnd  38305  ioorrnopnlem  46876  hoicvr  47120  hoidmvlelem3  47169  hspdifhsp  47188  hspmbllem2  47199