| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > fvresex | Structured version Visualization version GIF version | ||
| Description: Existence of the class of values of a restricted class. (Contributed by NM, 14-Nov-1995.) (Revised by Mario Carneiro, 11-Sep-2015.) |
| Ref | Expression |
|---|---|
| fvresex.1 | ⊢ 𝐴 ∈ V |
| Ref | Expression |
|---|---|
| fvresex | ⊢ {𝑦 ∣ ∃𝑥 𝑦 = ((𝐹 ↾ 𝐴)‘𝑥)} ∈ V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssv 3947 | . . . . . . . 8 ⊢ 𝐴 ⊆ V | |
| 2 | resmpt 5994 | . . . . . . . 8 ⊢ (𝐴 ⊆ V → ((𝑧 ∈ V ↦ (𝐹‘𝑧)) ↾ 𝐴) = (𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))) | |
| 3 | 1, 2 | ax-mp 5 | . . . . . . 7 ⊢ ((𝑧 ∈ V ↦ (𝐹‘𝑧)) ↾ 𝐴) = (𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧)) |
| 4 | 3 | fveq1i 6833 | . . . . . 6 ⊢ (((𝑧 ∈ V ↦ (𝐹‘𝑧)) ↾ 𝐴)‘𝑥) = ((𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))‘𝑥) |
| 5 | fveq2 6832 | . . . . . . . . 9 ⊢ (𝑧 = 𝑥 → (𝐹‘𝑧) = (𝐹‘𝑥)) | |
| 6 | eqid 2737 | . . . . . . . . 9 ⊢ (𝑧 ∈ V ↦ (𝐹‘𝑧)) = (𝑧 ∈ V ↦ (𝐹‘𝑧)) | |
| 7 | fvex 6845 | . . . . . . . . 9 ⊢ (𝐹‘𝑥) ∈ V | |
| 8 | 5, 6, 7 | fvmpt 6939 | . . . . . . . 8 ⊢ (𝑥 ∈ V → ((𝑧 ∈ V ↦ (𝐹‘𝑧))‘𝑥) = (𝐹‘𝑥)) |
| 9 | 8 | elv 3435 | . . . . . . 7 ⊢ ((𝑧 ∈ V ↦ (𝐹‘𝑧))‘𝑥) = (𝐹‘𝑥) |
| 10 | fveqres 6876 | . . . . . . 7 ⊢ (((𝑧 ∈ V ↦ (𝐹‘𝑧))‘𝑥) = (𝐹‘𝑥) → (((𝑧 ∈ V ↦ (𝐹‘𝑧)) ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑥)) | |
| 11 | 9, 10 | ax-mp 5 | . . . . . 6 ⊢ (((𝑧 ∈ V ↦ (𝐹‘𝑧)) ↾ 𝐴)‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑥) |
| 12 | 4, 11 | eqtr3i 2762 | . . . . 5 ⊢ ((𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))‘𝑥) = ((𝐹 ↾ 𝐴)‘𝑥) |
| 13 | 12 | eqeq2i 2750 | . . . 4 ⊢ (𝑦 = ((𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))‘𝑥) ↔ 𝑦 = ((𝐹 ↾ 𝐴)‘𝑥)) |
| 14 | 13 | exbii 1850 | . . 3 ⊢ (∃𝑥 𝑦 = ((𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))‘𝑥) ↔ ∃𝑥 𝑦 = ((𝐹 ↾ 𝐴)‘𝑥)) |
| 15 | 14 | abbii 2804 | . 2 ⊢ {𝑦 ∣ ∃𝑥 𝑦 = ((𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))‘𝑥)} = {𝑦 ∣ ∃𝑥 𝑦 = ((𝐹 ↾ 𝐴)‘𝑥)} |
| 16 | fvresex.1 | . . . 4 ⊢ 𝐴 ∈ V | |
| 17 | 16 | mptex 7169 | . . 3 ⊢ (𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧)) ∈ V |
| 18 | 17 | fvclex 7903 | . 2 ⊢ {𝑦 ∣ ∃𝑥 𝑦 = ((𝑧 ∈ 𝐴 ↦ (𝐹‘𝑧))‘𝑥)} ∈ V |
| 19 | 15, 18 | eqeltrri 2834 | 1 ⊢ {𝑦 ∣ ∃𝑥 𝑦 = ((𝐹 ↾ 𝐴)‘𝑥)} ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1542 ∃wex 1781 ∈ wcel 2114 {cab 2715 Vcvv 3430 ⊆ wss 3890 ↦ cmpt 5167 ↾ cres 5624 ‘cfv 6490 |
| 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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pr 5368 ax-un 7680 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5517 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |