Theorem ovprc1 7397

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ∅c0 4274  dom cdm 5622  Rel wrel 5627  (class class class)co 7358

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5628  df-rel 5629  df-dm 5632  df-iota 6446  df-fv 6498  df-ov 7361

This theorem is referenced by:  elfvov1  7400  mapssfset  8789  mapdom2  9077  relexpsucrd  14984  relexpsucld  14985  relexpreld  14991  relexpdmd  14995  relexprnd  14999  relexpfldd  15001  relexpaddd  15005  dfrtrclrec2  15009  relexpindlem  15014  oveqprc  17151  ressinbas  17204  ressress  17206  oduval  18243  oduleval  18244  gsum0  18641  efmndbas  18828  oppgval  19311  oppgplusfval  19312  mgpval  20113  opprval  20307  srasca  21165  rlmsca2  21184  dsmmval  21722  dsmmfi  21726  resspsrbas  21961  mpfrcl  22072  psrbaspropd  22207  mplbaspropd  22209  evl1fval1  22305  qtopres  23672  fgabs  23853  tngds  24622  tcphval  25194  of0r  32772  erlval  33339  fracval  33385  resvsca  33412  mapco2g  43157  mzpmfp  43190  mendbas  43623  naryfvalixp  49102  1aryenef  49118  2aryenef  49129  resccat  49546