Theorem ovprc1 7469

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  Vcvv 3477  ∅c0 4338  dom cdm 5688  Rel wrel 5693  (class class class)co 7430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-xp 5694  df-rel 5695  df-dm 5698  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  elfvov1  7472  mapssfset  8889  mapdom2  9186  relexpsucrd  15068  relexpsucld  15069  relexpreld  15075  relexpdmd  15079  relexprnd  15083  relexpfldd  15085  relexpaddd  15089  dfrtrclrec2  15093  relexpindlem  15098  oveqprc  17225  setsnidOLD  17243  ressbasOLD  17280  resslemOLD  17287  ressinbas  17290  ressress  17293  oduval  18344  oduleval  18345  gsum0  18709  efmndbas  18896  oppgval  19377  oppgplusfval  19378  mgpval  20154  opprval  20351  srasca  21200  srascaOLD  21201  rlmsca2  21223  dsmmval  21771  dsmmfi  21775  resspsrbas  22011  mpfrcl  22126  psrbaspropd  22251  mplbaspropd  22253  evl1fval1  22350  qtopres  23721  fgabs  23902  tnglemOLD  24669  tngds  24683  tngdsOLD  24684  tcphval  25265  of0r  32694  erlval  33244  fracval  33285  resvsca  33335  resvlemOLD  33337  mapco2g  42701  mzpmfp  42734  mendbas  43168  naryfvalixp  48478  1aryenef  48494  2aryenef  48505