Theorem ovprc2 7408

Description: The value of an operation when the second argument is a proper class. (Contributed by Mario Carneiro, 26-Apr-2015.)

Hypothesis

Ref	Expression
ovprc1.1	⊢ Rel dom 𝐹

Assertion

Ref	Expression
ovprc2	⊢ (¬ 𝐵 ∈ V → (𝐴𝐹𝐵) = ∅)

Proof of Theorem ovprc2

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐵 ∈ V)
2		ovprc1.1	. . 3 ⊢ Rel dom 𝐹
3	2	ovprc 7406	. 2 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅)
4	1, 3	nsyl5 159	1 ⊢ (¬ 𝐵 ∈ V → (𝐴𝐹𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ∅c0 4287  dom cdm 5632  Rel wrel 5637  (class class class)co 7368

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 5243  ax-nul 5253  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-dm 5642  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  elfvov2  7411  ressbasssg  17176  ressbasssOLD  17179  ress0  17182  wunress  17188  0rest  17361  firest  17364  subcmn  19778  dprdval0prc  19945  submomnd  20073  suborng  20821  zrhval  21474  dsmmval2  21703  psrbas  21901  psr1val  22138  vr1val  22144  ply1ascl  22212  evl1fval  22284  restbas  23114  resstopn  23142  deg1fval  26053  wwlksn  29922  bj-restsnid  37340  1aryenef  49005  2aryenef  49016  prcof1  49747