Theorem ovprc1 7407

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ∅c0 4287  dom cdm 5632  Rel wrel 5637  (class class class)co 7368

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-dm 5642  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  elfvov1  7410  mapssfset  8800  mapdom2  9088  relexpsucrd  14968  relexpsucld  14969  relexpreld  14975  relexpdmd  14979  relexprnd  14983  relexpfldd  14985  relexpaddd  14989  dfrtrclrec2  14993  relexpindlem  14998  oveqprc  17131  ressinbas  17184  ressress  17186  oduval  18223  oduleval  18224  gsum0  18621  efmndbas  18808  oppgval  19288  oppgplusfval  19289  mgpval  20090  opprval  20286  srasca  21144  rlmsca2  21163  dsmmval  21701  dsmmfi  21705  resspsrbas  21941  mpfrcl  22052  psrbaspropd  22187  mplbaspropd  22189  evl1fval1  22287  qtopres  23654  fgabs  23835  tngds  24604  tcphval  25186  of0r  32769  erlval  33352  fracval  33398  resvsca  33425  mapco2g  43071  mzpmfp  43104  mendbas  43537  naryfvalixp  48989  1aryenef  49005  2aryenef  49016  resccat  49433