Theorem ovprc1 7450

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1567   ∈ wcel 2149  Vcvv 3463  ∅c0 4294  dom cdm 5662  Rel wrel 5667  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-xp 5668  df-rel 5669  df-dm 5672  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  elfvov1  7453  mapssfset  8847  mapdom2  9135  relexpsucrd  15069  relexpsucld  15070  relexpreld  15076  relexpdmd  15080  relexprnd  15084  relexpfldd  15086  relexpaddd  15090  dfrtrclrec2  15094  relexpindlem  15099  oveqprc  17251  ressinbas  17304  ressress  17306  oduval  18343  oduleval  18344  gsum0  18741  efmndbas  18929  oppgval  19416  oppgplusfval  19417  mgpval  20218  opprval  20419  srasca  21278  rlmsca2  21297  dsmmval  21852  dsmmfi  21856  resspsrbas  22091  mpfrcl  22204  psrbaspropd  22362  mplbaspropd  22364  evl1fval1  22459  qtopres  23823  fgabs  24004  tngds  24773  tcphval  25345  of0r  32964  erlval  33518  fracval  33567  resvsca  33594  mapco2g  43336  mzpmfp  43369  mendbas  43798  naryfvalixp  49293  1aryenef  49309  2aryenef  49320  resccat  49736