| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > ovexg | GIF version | ||
| Description: Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.) |
| Ref | Expression |
|---|---|
| ovexg | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐹𝐵) ∈ V) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ov 5947 | . 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | |
| 2 | simp2 1001 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → 𝐹 ∈ 𝑊) | |
| 3 | opexg 4272 | . . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋) → 〈𝐴, 𝐵〉 ∈ V) | |
| 4 | 3 | 3adant2 1019 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → 〈𝐴, 𝐵〉 ∈ V) |
| 5 | fvexg 5595 | . . 3 ⊢ ((𝐹 ∈ 𝑊 ∧ 〈𝐴, 𝐵〉 ∈ V) → (𝐹‘〈𝐴, 𝐵〉) ∈ V) | |
| 6 | 2, 4, 5 | syl2anc 411 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (𝐹‘〈𝐴, 𝐵〉) ∈ V) |
| 7 | 1, 6 | eqeltrid 2292 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐹𝐵) ∈ V) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ∧ w3a 981 ∈ wcel 2176 Vcvv 2772 〈cop 3636 ‘cfv 5271 (class class class)co 5944 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-sep 4162 ax-pow 4218 ax-pr 4253 ax-un 4480 |
| This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ral 2489 df-rex 2490 df-v 2774 df-un 3170 df-in 3172 df-ss 3179 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-br 4045 df-opab 4106 df-cnv 4683 df-dm 4685 df-rn 4686 df-iota 5232 df-fv 5279 df-ov 5947 |
| This theorem is referenced by: mapxpen 6945 seq1g 10608 seqp1g 10611 seqclg 10617 seqm1g 10619 seqfeq4g 10676 prdsplusgfval 13116 prdsmulrfval 13118 imasex 13137 imasival 13138 imasbas 13139 imasplusg 13140 imasmulr 13141 imasaddfnlemg 13146 imasaddvallemg 13147 plusfvalg 13195 plusffng 13197 gsumsplit1r 13230 gsumprval 13231 gsumfzz 13327 gsumwsubmcl 13328 gsumfzcl 13331 grpsubval 13378 mulgval 13458 mulgfng 13460 mulgnngsum 13463 mulg1 13465 mulgnnp1 13466 mulgnndir 13487 subgintm 13534 subrngintm 13974 scafvalg 14069 scaffng 14071 rmodislmodlem 14112 rmodislmod 14113 lsssn0 14132 lss1d 14145 lssintclm 14146 ellspsn 14179 crngridl 14292 metrest 14978 |
| Copyright terms: Public domain | W3C validator |