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

Theorem ovprc1 7390
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 7389 . 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 3443  c0 4280  dom cdm 5631  Rel wrel 5636  (class class class)co 7351
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 2708  ax-sep 5254  ax-nul 5261  ax-pr 5382
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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-xp 5637  df-rel 5638  df-dm 5641  df-iota 6445  df-fv 6501  df-ov 7354
This theorem is referenced by:  mapssfset  8747  mapdom2  9050  relexpsucrd  14878  relexpsucld  14879  relexpreld  14885  relexpdmd  14889  relexprnd  14893  relexpfldd  14895  relexpaddd  14899  dfrtrclrec2  14903  relexpindlem  14908  oveqprc  17024  setsnidOLD  17042  ressbasOLD  17079  resslemOLD  17083  ressinbas  17086  ressress  17089  oduval  18137  oduleval  18138  gsum0  18499  efmndbas  18641  oppgval  19084  oppgplusfval  19085  mgpval  19858  opprval  20003  srasca  20599  srascaOLD  20600  rlmsca2  20623  dsmmval  21093  dsmmfi  21097  resspsrbas  21336  mpfrcl  21447  psrbaspropd  21558  mplbaspropd  21560  evl1fval1  21649  qtopres  23001  fgabs  23182  tnglemOLD  23949  tngds  23963  tngdsOLD  23964  tcphval  24534  resvsca  31947  resvlemOLD  31949  mapco2g  40946  mzpmfp  40979  mendbas  41420  naryfvalixp  46616  1aryenef  46632  2aryenef  46643
  Copyright terms: Public domain W3C validator