![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ovprc1 | Structured version Visualization version GIF version |
Description: The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.) |
Ref | Expression |
---|---|
ovprc1.1 | ⊢ Rel dom 𝐹 |
Ref | Expression |
---|---|
ovprc1 | ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 483 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐴 ∈ V) | |
2 | ovprc1.1 | . . 3 ⊢ Rel dom 𝐹 | |
3 | 2 | ovprc 7392 | . 2 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅) |
4 | 1, 3 | nsyl5 159 | 1 ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 Vcvv 3444 ∅c0 4281 dom cdm 5632 Rel wrel 5637 (class class class)co 7354 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5255 ax-nul 5262 ax-pr 5383 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-opab 5167 df-xp 5638 df-rel 5639 df-dm 5642 df-iota 6446 df-fv 6502 df-ov 7357 |
This theorem is referenced by: mapssfset 8786 mapdom2 9089 relexpsucrd 14915 relexpsucld 14916 relexpreld 14922 relexpdmd 14926 relexprnd 14930 relexpfldd 14932 relexpaddd 14936 dfrtrclrec2 14940 relexpindlem 14945 oveqprc 17061 setsnidOLD 17079 ressbasOLD 17116 resslemOLD 17120 ressinbas 17123 ressress 17126 oduval 18174 oduleval 18175 gsum0 18536 efmndbas 18678 oppgval 19121 oppgplusfval 19122 mgpval 19895 opprval 20046 srasca 20642 srascaOLD 20643 rlmsca2 20666 dsmmval 21136 dsmmfi 21140 resspsrbas 21380 mpfrcl 21491 psrbaspropd 21602 mplbaspropd 21604 evl1fval1 21693 qtopres 23045 fgabs 23226 tnglemOLD 23993 tngds 24007 tngdsOLD 24008 tcphval 24578 resvsca 32016 resvlemOLD 32018 mapco2g 41013 mzpmfp 41046 mendbas 41487 naryfvalixp 46685 1aryenef 46701 2aryenef 46712 |
Copyright terms: Public domain | W3C validator |