Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elixp | Structured version Visualization version GIF version |
Description: Membership in an infinite Cartesian product. (Contributed by NM, 28-Sep-2006.) |
Ref | Expression |
---|---|
elixp.1 | ⊢ 𝐹 ∈ V |
Ref | Expression |
---|---|
elixp | ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elixp2 8606 | . 2 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | |
2 | elixp.1 | . . 3 ⊢ 𝐹 ∈ V | |
3 | 3anass 1097 | . . 3 ⊢ ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))) | |
4 | 2, 3 | mpbiran 709 | . 2 ⊢ ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
5 | 1, 4 | bitri 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 |