Theorem ovprc1 7314

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

Step	Hyp	Ref	Expression
1		simpl 483	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐴 ∈ V)
2		ovprc1.1	. . 3 ⊢ Rel dom 𝐹
3	2	ovprc 7313	. 2 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅)
4	1, 3	nsyl5 159	1 ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  Vcvv 3432  ∅c0 4256  dom cdm 5589  Rel wrel 5594  (class class class)co 7275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-xp 5595  df-rel 5596  df-dm 5599  df-iota 6391  df-fv 6441  df-ov 7278

This theorem is referenced by:  mapssfset  8639  mapdom2  8935  relexpsucrd  14744  relexpsucld  14745  relexpreld  14751  relexpdmd  14755  relexprnd  14759  relexpfldd  14761  relexpaddd  14765  dfrtrclrec2  14769  relexpindlem  14774  oveqprc  16893  setsnidOLD  16911  ressbasOLD  16948  resslemOLD  16952  ressinbas  16955  ressress  16958  oduval  18006  oduleval  18007  gsum0  18368  efmndbas  18510  oppgval  18951  oppgplusfval  18952  mgpval  19723  opprval  19863  srasca  20447  srascaOLD  20448  rlmsca2  20471  dsmmval  20941  dsmmfi  20945  resspsrbas  21184  mpfrcl  21295  psrbaspropd  21406  mplbaspropd  21408  evl1fval1  21497  qtopres  22849  fgabs  23030  tnglemOLD  23797  tngds  23811  tngdsOLD  23812  tcphval  24382  resvsca  31529  resvlemOLD  31531  mapco2g  40536  mzpmfp  40569  mendbas  41009  naryfvalixp  45975  1aryenef  45991  2aryenef  46002