![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fovcl | Structured version Visualization version GIF version |
Description: Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Proof shortened by AV, 9-Mar-2025.) |
Ref | Expression |
---|---|
fovcl.1 | ⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 |
Ref | Expression |
---|---|
fovcl | ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fovcl.1 | . . . 4 ⊢ 𝐹:(𝑅 × 𝑆)⟶𝐶 | |
2 | 1 | a1i 11 | . . 3 ⊢ (𝐴 ∈ 𝑅 → 𝐹:(𝑅 × 𝑆)⟶𝐶) |
3 | 2 | fovcld 7528 | . 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
4 | 3 | 3anidm12 1416 | 1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (𝐴𝐹𝐵) ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2098 × cxp 5664 ⟶wf 6529 (class class class)co 7401 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pr 5417 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-iun 4989 df-br 5139 df-opab 5201 df-mpt 5222 df-id 5564 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-fv 6541 df-ov 7404 |
This theorem is referenced by: addclnq 10936 mulclnq 10938 adderpq 10947 mulerpq 10948 distrnq 10952 axaddcl 11142 axmulcl 11144 xaddcl 13215 xmulcl 13249 elfzoelz 13629 addcnlem 24702 sgmcl 26994 hvaddcl 30734 hvmulcl 30735 hicl 30802 hhssabloilem 30983 gg-cncrng 35673 rmxynorm 42146 rmxyneg 42148 rmxy1 42150 rmxy0 42151 rmxp1 42160 rmyp1 42161 rmxm1 42162 rmym1 42163 rmxluc 42164 rmyluc 42165 rmyluc2 42166 rmxdbl 42167 rmydbl 42168 rmxypos 42175 ltrmynn0 42176 ltrmxnn0 42177 lermxnn0 42178 rmxnn 42179 ltrmy 42180 rmyeq0 42181 rmyeq 42182 lermy 42183 rmynn 42184 rmynn0 42185 rmyabs 42186 jm2.24nn 42187 jm2.17a 42188 jm2.17b 42189 jm2.17c 42190 jm2.24 42191 rmygeid 42192 jm2.18 42216 jm2.19lem1 42217 jm2.19lem2 42218 jm2.19 42221 jm2.22 42223 jm2.23 42224 jm2.20nn 42225 jm2.25 42227 jm2.26a 42228 jm2.26lem3 42229 jm2.26 42230 jm2.15nn0 42231 jm2.16nn0 42232 jm2.27a 42233 jm2.27c 42235 rmydioph 42242 rmxdiophlem 42243 jm3.1lem1 42245 jm3.1 42248 expdiophlem1 42249 |
Copyright terms: Public domain | W3C validator |