Theorem ovprc1 7294

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 482	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐴 ∈ V)
2		ovprc1.1	. . 3 ⊢ Rel dom 𝐹
3	2	ovprc 7293	. 2 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅)
4	1, 3	nsyl5 159	1 ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3422  ∅c0 4253  dom cdm 5580  Rel wrel 5585  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-xp 5586  df-rel 5587  df-dm 5590  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  mapssfset  8597  mapdom2  8884  relexpsucrd  14672  relexpsucld  14673  relexpreld  14679  relexpdmd  14683  relexprnd  14687  relexpfldd  14689  relexpaddd  14693  dfrtrclrec2  14697  relexpindlem  14702  oveqprc  16821  setsnidOLD  16839  ressbasOLD  16874  resslemOLD  16878  ressinbas  16881  ressress  16884  oduval  17922  oduleval  17923  gsum0  18283  efmndbas  18425  oppgval  18866  oppgplusfval  18867  mgpval  19638  opprval  19778  srasca  20362  rlmsca2  20384  dsmmval  20851  dsmmfi  20855  resspsrbas  21094  mpfrcl  21205  psrbaspropd  21316  mplbaspropd  21318  evl1fval1  21407  qtopres  22757  fgabs  22938  tnglemOLD  23703  tngds  23717  tngdsOLD  23718  tcphval  24287  resvsca  31431  resvlemOLD  31433  mapco2g  40452  mzpmfp  40485  mendbas  40925  naryfvalixp  45863  1aryenef  45879  2aryenef  45890