Theorem ovprc1 7470

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3480  ∅c0 4333  dom cdm 5685  Rel wrel 5690  (class class class)co 7431

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-dm 5695  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  elfvov1  7473  mapssfset  8891  mapdom2  9188  relexpsucrd  15072  relexpsucld  15073  relexpreld  15079  relexpdmd  15083  relexprnd  15087  relexpfldd  15089  relexpaddd  15093  dfrtrclrec2  15097  relexpindlem  15102  oveqprc  17229  setsnidOLD  17246  ressbasOLD  17281  resslemOLD  17288  ressinbas  17291  ressress  17293  oduval  18333  oduleval  18334  gsum0  18697  efmndbas  18884  oppgval  19365  oppgplusfval  19366  mgpval  20140  opprval  20335  srasca  21183  srascaOLD  21184  rlmsca2  21206  dsmmval  21754  dsmmfi  21758  resspsrbas  21994  mpfrcl  22109  psrbaspropd  22236  mplbaspropd  22238  evl1fval1  22335  qtopres  23706  fgabs  23887  tnglemOLD  24654  tngds  24668  tngdsOLD  24669  tcphval  25252  of0r  32688  erlval  33262  fracval  33306  resvsca  33356  resvlemOLD  33358  mapco2g  42725  mzpmfp  42758  mendbas  43192  naryfvalixp  48550  1aryenef  48566  2aryenef  48577