| 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 482 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐴 ∈ V) | |
| 2 | ovprc1.1 | . . 3 ⊢ Rel dom 𝐹 | |
| 3 | 2 | ovprc 7469 | . 2 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅) |
| 4 | 1, 3 | nsyl5 159 | 1 ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 Vcvv 3480 ∅c0 4333 dom cdm 5685 Rel wrel 5690 (class class class)co 7431 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-xp 5691 df-rel 5692 df-dm 5695 df-iota 6514 df-fv 6569 df-ov 7434 |
| This theorem is referenced by: elfvov1 7473 mapssfset 8891 mapdom2 9188 relexpsucrd 15072 relexpsucld 15073 relexpreld 15079 relexpdmd 15083 relexprnd 15087 relexpfldd 15089 relexpaddd 15093 dfrtrclrec2 15097 relexpindlem 15102 oveqprc 17229 setsnidOLD 17246 ressbasOLD 17281 resslemOLD 17288 ressinbas 17291 ressress 17293 oduval 18333 oduleval 18334 gsum0 18697 efmndbas 18884 oppgval 19365 oppgplusfval 19366 mgpval 20140 opprval 20335 srasca 21183 srascaOLD 21184 rlmsca2 21206 dsmmval 21754 dsmmfi 21758 resspsrbas 21994 mpfrcl 22109 psrbaspropd 22236 mplbaspropd 22238 evl1fval1 22335 qtopres 23706 fgabs 23887 tnglemOLD 24654 tngds 24668 tngdsOLD 24669 tcphval 25252 of0r 32688 erlval 33262 fracval 33306 resvsca 33356 resvlemOLD 33358 mapco2g 42725 mzpmfp 42758 mendbas 43192 naryfvalixp 48550 1aryenef 48566 2aryenef 48577 |
| Copyright terms: Public domain | W3C validator |