| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > elixp2 | Structured version Visualization version GIF version | ||
| Description: Membership in an infinite Cartesian product. See df-ixp 8884 for discussion of the notation. (Contributed by NM, 28-Sep-2006.) |
| Ref | Expression |
|---|---|
| elixp2 | ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fneq1 6616 | . . . . 5 ⊢ (𝑓 = 𝐹 → (𝑓 Fn 𝐴 ↔ 𝐹 Fn 𝐴)) | |
| 2 | fveq1 6870 | . . . . . . 7 ⊢ (𝑓 = 𝐹 → (𝑓‘𝑥) = (𝐹‘𝑥)) | |
| 3 | 2 | eleq1d 2850 | . . . . . 6 ⊢ (𝑓 = 𝐹 → ((𝑓‘𝑥) ∈ 𝐵 ↔ (𝐹‘𝑥) ∈ 𝐵)) |
| 4 | 3 | ralbidv 3188 | . . . . 5 ⊢ (𝑓 = 𝐹 → (∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
| 5 | 1, 4 | anbi12d 643 | . . . 4 ⊢ (𝑓 = 𝐹 → ((𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵) ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))) |
| 6 | dfixp 8885 | . . . 4 ⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑓 ∣ (𝑓 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝐵)} | |
| 7 | 5, 6 | elab2g 3642 | . . 3 ⊢ (𝐹 ∈ V → (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))) |
| 8 | 7 | pm5.32i 584 | . 2 ⊢ ((𝐹 ∈ V ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))) |
| 9 | elex 3478 | . . 3 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 → 𝐹 ∈ V) | |
| 10 | 9 | pm4.71ri 569 | . 2 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 ∈ X𝑥 ∈ 𝐴 𝐵)) |
| 11 | 3anass 1109 | . 2 ⊢ ((𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵) ↔ (𝐹 ∈ V ∧ (𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵))) | |
| 12 | 8, 10, 11 | 3bitr4i 306 | 1 ⊢ (𝐹 ∈ X𝑥 ∈ 𝐴 𝐵 ↔ (𝐹 ∈ V ∧ 𝐹 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ 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: fvixp 8888 ixpfn 8889 elixp 8890 ixpf 8906 resixp 8919 undifixp 8920 mptelixpg 8921 prdsbasprj 17515 xpsfrnel 17606 xpscf 17609 isssc 17867 isfuncd 17912 funcres2b 17944 dprdw 20073 ptrecube 38131 kelac1 43652 elixpconstg 45665 fvixp2 45774 rrxsnicc 46872 ioorrnopnxrlem 46878 hoiqssbllem1 47194 iinhoiicclem 47245 iunhoiioolem 47247 funcf2lem 49710 isnatd 49852 |
| Copyright terms: Public domain | W3C validator |