Theorem ovprc1 7457

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 7456	. 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 3451  ∅c0 4279  dom cdm 5651  Rel wrel 5656  (class class class)co 7418

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-rel 5658  df-dm 5661  df-iota 6493  df-fv 6545  df-ov 7421

This theorem is used by:  elfvov1  7460  mapssfset  8866  mapdom2  9160  relexpsucrd  15179  relexpsucld  15180  relexpreld  15186  relexpdmd  15190  relexprnd  15194  relexpfldd  15196  relexpaddd  15200  dfrtrclrec2  15204  relexpindlem  15209  oveqprc  17363  ressinbas  17416  ressress  17418  oduval  18455  oduleval  18456  gsum0  18866  efmndbas  19060  oppgval  19554  oppgplusfval  19555  mgpval  20356  opprval  20561  srasca  21448  rlmsca2  21467  dsmmval  22033  dsmmfi  22037  resspsrbas  22274  mpfrcl  22387  psrbaspropd  22545  mplbaspropd  22547  evl1fval1  22642  qtopres  24010  fgabs  24191  tngds  24960  tcphval  25532  of0r  33266  erlval  33812  fracval  33859  resvsca  33886  mapco2g  43704  mzpmfp  43737  mendbas  44166  naryfvalixp  49710  1aryenef  49726  2aryenef  49737  resccat  50151