Theorem ovprc1 7490

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Vcvv 3454  ∅c0 4281  dom cdm 5658  Rel wrel 5663  (class class class)co 7451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-rel 5665  df-dm 5668  df-iota 6520  df-fv 6574  df-ov 7454

This theorem is used by:  elfvov1  7493  mapssfset  8911  mapdom2  9205  relexpsucrd  15229  relexpsucld  15230  relexpreld  15236  relexpdmd  15240  relexprnd  15244  relexpfldd  15246  relexpaddd  15250  dfrtrclrec2  15254  relexpindlem  15259  oveqprc  17414  ressinbas  17467  ressress  17469  oduval  18512  oduleval  18513  gsum0  18923  efmndbas  19117  oppgval  19612  oppgplusfval  19613  mgpval  20414  opprval  20619  srasca  21506  rlmsca2  21525  dsmmval  22095  dsmmfi  22099  resspsrbas  22336  mpfrcl  22449  psrbaspropd  22607  mplbaspropd  22609  evl1fval1  22704  qtopres  24072  fgabs  24253  tngds  25022  tcphval  25594  of0r  33370  erlval  33918  fracval  33970  resvsca  33997  mapco2g  43991  mzpmfp  44024  mendbas  44443  naryfvalixp  50072  1aryenef  50088  2aryenef  50099  resccat  50519