Theorem elixp 8838

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109  ∀wral 3044  Vcvv 3438   Fn wfn 6481  ‘cfv 6486  Xcixp 8831

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fn 6489  df-fv 6494  df-ixp 8832

This theorem is referenced by:  elixpconst  8839  ixpin  8857  ixpiin  8858  resixpfo  8870  elixpsn  8871  boxriin  8874  boxcutc  8875  ixpfi2  9259  ixpiunwdom  9501  dfac9  10050  ac9  10396  ac9s  10406  konigthlem  10481  cofucl  17813  yonedalem3  18204  psrbaglefi  21851  ptpjpre1  23474  ptpjcn  23514  ptpjopn  23515  ptclsg  23518  dfac14  23521  pthaus  23541  xkopt  23558  ptcmplem2  23956  ptcmplem3  23957  ptcmplem4  23958  prdsbl  24395  prdsxmslem2  24433  eulerpartlemb  34335  ptpconn  35205  finixpnum  37584  ptrest  37598  poimirlem29  37628  poimirlem30  37629  inixp  37707  prdstotbnd  37773  ioorrnopnlem  46286  hoicvr  46530  hoidmvlelem3  46579  hspdifhsp  46598  hspmbllem2  46609