Theorem ovprc1 7452

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 7451	. 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 2145  Vcvv 3450  ∅c0 4279  dom cdm 5655  Rel wrel 5660  (class class class)co 7413

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-nul 5263  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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-rel 5662  df-dm 5665  df-iota 6489  df-fv 6541  df-ov 7416

This theorem is used by:  elfvov1  7455  mapssfset  8852  mapdom2  9146  relexpsucrd  15106  relexpsucld  15107  relexpreld  15113  relexpdmd  15117  relexprnd  15121  relexpfldd  15123  relexpaddd  15127  dfrtrclrec2  15131  relexpindlem  15136  oveqprc  17284  ressinbas  17337  ressress  17339  oduval  18376  oduleval  18377  gsum0  18786  efmndbas  18980  oppgval  19474  oppgplusfval  19475  mgpval  20276  opprval  20479  srasca  21364  rlmsca2  21383  dsmmval  21947  dsmmfi  21951  resspsrbas  22188  mpfrcl  22301  psrbaspropd  22459  mplbaspropd  22461  evl1fval1  22556  qtopres  23924  fgabs  24105  tngds  24874  tcphval  25446  of0r  33152  erlval  33698  fracval  33745  resvsca  33772  mapco2g  43559  mzpmfp  43592  mendbas  44021  naryfvalixp  49559  1aryenef  49575  2aryenef  49586  resccat  50000