Theorem ovprc1 7426

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3447  ∅c0 4296  dom cdm 5638  Rel wrel 5643  (class class class)co 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-rel 5645  df-dm 5648  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  elfvov1  7429  mapssfset  8824  mapdom2  9112  relexpsucrd  14999  relexpsucld  15000  relexpreld  15006  relexpdmd  15010  relexprnd  15014  relexpfldd  15016  relexpaddd  15020  dfrtrclrec2  15024  relexpindlem  15029  oveqprc  17162  ressinbas  17215  ressress  17217  oduval  18249  oduleval  18250  gsum0  18611  efmndbas  18798  oppgval  19279  oppgplusfval  19280  mgpval  20052  opprval  20247  srasca  21087  rlmsca2  21106  dsmmval  21643  dsmmfi  21647  resspsrbas  21883  mpfrcl  21992  psrbaspropd  22119  mplbaspropd  22121  evl1fval1  22218  qtopres  23585  fgabs  23766  tngds  24536  tcphval  25118  of0r  32602  erlval  33209  fracval  33254  resvsca  33304  mapco2g  42702  mzpmfp  42735  mendbas  43169  naryfvalixp  48618  1aryenef  48634  2aryenef  48645  resccat  49063