![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ovprc2 | Structured version Visualization version GIF version |
Description: The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
ovprc1.1 | ⊢ Rel dom 𝐹 |
Ref | Expression |
---|---|
ovprc2 | ⊢ (¬ 𝐵 ∈ V → (𝐴𝐹𝐵) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr 478 | . . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐵 ∈ V) | |
2 | 1 | con3i 152 | . 2 ⊢ (¬ 𝐵 ∈ V → ¬ (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
3 | ovprc1.1 | . . 3 ⊢ Rel dom 𝐹 | |
4 | 3 | ovprc 6915 | . 2 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅) |
5 | 2, 4 | syl 17 | 1 ⊢ (¬ 𝐵 ∈ V → (𝐴𝐹𝐵) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 385 = wceq 1653 ∈ wcel 2157 Vcvv 3385 ∅c0 4115 dom cdm 5312 Rel wrel 5317 (class class class)co 6878 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2377 ax-ext 2777 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5097 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2591 df-eu 2609 df-clab 2786 df-cleq 2792 df-clel 2795 df-nfc 2930 df-ral 3094 df-rex 3095 df-rab 3098 df-v 3387 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-nul 4116 df-if 4278 df-sn 4369 df-pr 4371 df-op 4375 df-uni 4629 df-br 4844 df-opab 4906 df-xp 5318 df-rel 5319 df-dm 5322 df-iota 6064 df-fv 6109 df-ov 6881 |
This theorem is referenced by: ressbasss 16257 ress0 16259 wunress 16266 0rest 16405 firest 16408 subcmn 18557 dprdval0prc 18717 psrbas 19701 psr1val 19878 vr1val 19884 ply1ascl 19950 evl1fval 20014 zrhval 20178 dsmmval2 20405 restbas 21291 resstopn 21319 deg1fval 24181 wwlksn 27088 clwwlknOLD 27331 submomnd 30226 suborng 30331 bj-restsnid 33533 |
Copyright terms: Public domain | W3C validator |