Theorem ovprc1 7401

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3446  ∅c0 4287  dom cdm 5638  Rel wrel 5643  (class class class)co 7362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-xp 5644  df-rel 5645  df-dm 5648  df-iota 6453  df-fv 6509  df-ov 7365

This theorem is referenced by:  mapssfset  8796  mapdom2  9099  relexpsucrd  14930  relexpsucld  14931  relexpreld  14937  relexpdmd  14941  relexprnd  14945  relexpfldd  14947  relexpaddd  14951  dfrtrclrec2  14955  relexpindlem  14960  oveqprc  17075  setsnidOLD  17093  ressbasOLD  17130  resslemOLD  17137  ressinbas  17140  ressress  17143  oduval  18191  oduleval  18192  gsum0  18553  efmndbas  18695  oppgval  19139  oppgplusfval  19140  mgpval  19913  opprval  20064  srasca  20705  srascaOLD  20706  rlmsca2  20729  dsmmval  21177  dsmmfi  21181  resspsrbas  21421  mpfrcl  21532  psrbaspropd  21643  mplbaspropd  21645  evl1fval1  21734  qtopres  23086  fgabs  23267  tnglemOLD  24034  tngds  24048  tngdsOLD  24049  tcphval  24619  resvsca  32192  resvlemOLD  32194  mapco2g  41095  mzpmfp  41128  mendbas  41569  naryfvalixp  46835  1aryenef  46851  2aryenef  46862