Theorem elixp 8894

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 8891	. 2 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
2		elixp.1	. . 3 ⊢ 𝐹 ∈ V
3		3anass 1095	. . 3 ⊢ ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)))
4	2, 3	mpbiran 707	. 2 ⊢ ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))
5	1, 4	bitri 274	1 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   ∈ wcel 2106  ∀wral 3061  Vcvv 3474   Fn wfn 6535  ‘cfv 6540  Xcixp 8887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6492  df-fun 6542  df-fn 6543  df-fv 6548  df-ixp 8888

This theorem is referenced by:  elixpconst  8895  ixpin  8913  ixpiin  8914  resixpfo  8926  elixpsn  8927  boxriin  8930  boxcutc  8931  ixpfi2  9346  ixpiunwdom  9581  dfac9  10127  ac9  10474  ac9s  10484  konigthlem  10559  cofucl  17834  yonedalem3  18229  psrbaglefi  21476  psrbaglefiOLD  21477  ptpjpre1  23066  ptpjcn  23106  ptpjopn  23107  ptclsg  23110  dfac14  23113  pthaus  23133  xkopt  23150  ptcmplem2  23548  ptcmplem3  23549  ptcmplem4  23550  prdsbl  23991  prdsxmslem2  24029  eulerpartlemb  33355  ptpconn  34212  finixpnum  36461  ptrest  36475  poimirlem29  36505  poimirlem30  36506  inixp  36584  prdstotbnd  36650  ioorrnopnlem  45006  hoicvr  45250  hoidmvlelem3  45299  hspdifhsp  45318  hspmbllem2  45329