![]() |
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 8448 | . 2 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) | |
2 | elixp.1 | . . 3 ⊢ 𝐹 ∈ V | |
3 | 3anass 1092 | . . 3 ⊢ ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))) | |
4 | 2, 3 | mpbiran 708 | . 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 1084 ∈ wcel 2111 ∀wral 3106 Vcvv 3441 Fn wfn 6319 ‘cfv 6324 Xcixp 8444 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-v 3443 df-un 3886 df-in 3888 df-ss 3898 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6283 df-fun 6326 df-fn 6327 df-fv 6332 df-ixp 8445 |
This theorem is referenced by: elixpconst 8452 ixpin 8470 ixpiin 8471 resixpfo 8483 elixpsn 8484 boxriin 8487 boxcutc 8488 ixpfi2 8806 ixpiunwdom 9038 dfac9 9547 ac9 9894 ac9s 9904 konigthlem 9979 cofucl 17150 yonedalem3 17522 psrbaglefi 20610 ptpjpre1 22176 ptpjcn 22216 ptpjopn 22217 ptclsg 22220 dfac14 22223 pthaus 22243 xkopt 22260 ptcmplem2 22658 ptcmplem3 22659 ptcmplem4 22660 prdsbl 23098 prdsxmslem2 23136 eulerpartlemb 31736 ptpconn 32593 finixpnum 35042 ptrest 35056 poimirlem29 35086 poimirlem30 35087 inixp 35166 prdstotbnd 35232 ioorrnopnlem 42946 hoicvr 43187 hoidmvlelem3 43236 hspdifhsp 43255 hspmbllem2 43266 |
Copyright terms: Public domain | W3C validator |