Theorem ovprc1 7449

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Vcvv 3455  ∅c0 4286  dom cdm 5661  Rel wrel 5666  (class class class)co 7410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-rel 5668  df-dm 5671  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is referenced by:  elfvov1  7452  mapssfset  8844  mapdom2  9132  relexpsucrd  15066  relexpsucld  15067  relexpreld  15073  relexpdmd  15077  relexprnd  15081  relexpfldd  15083  relexpaddd  15087  dfrtrclrec2  15091  relexpindlem  15096  oveqprc  17247  ressinbas  17300  ressress  17302  oduval  18339  oduleval  18340  gsum0  18737  efmndbas  18925  oppgval  19412  oppgplusfval  19413  mgpval  20214  opprval  20416  srasca  21301  rlmsca2  21320  dsmmval  21884  dsmmfi  21888  resspsrbas  22123  mpfrcl  22236  psrbaspropd  22394  mplbaspropd  22396  evl1fval1  22491  qtopres  23855  fgabs  24036  tngds  24805  tcphval  25377  of0r  33024  erlval  33578  fracval  33625  resvsca  33652  mapco2g  43445  mzpmfp  43478  mendbas  43907  naryfvalixp  49409  1aryenef  49425  2aryenef  49436  resccat  49852