MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovprc1 Structured version   Visualization version   GIF version

Theorem ovprc1 7393
Description: The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.)
Hypothesis
Ref Expression
ovprc1.1 Rel dom 𝐹
Assertion
Ref Expression
ovprc1 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)

Proof of Theorem ovprc1
StepHypRef Expression
1 simpl 483 . 2 ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐴 ∈ V)
2 ovprc1.1 . . 3 Rel dom 𝐹
32ovprc 7392 . 2 (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅)
41, 3nsyl5 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