Theorem ovprc 7306

Description: The value of an operation when the one of the arguments is a proper class. Note: this theorem is dependent on our particular definitions of operation value, function value, and ordered pair. (Contributed by Mario Carneiro, 26-Apr-2015.)

Hypothesis

Ref	Expression
ovprc1.1	⊢ Rel dom 𝐹

Assertion

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

Proof of Theorem ovprc

Step	Hyp	Ref	Expression
1		df-ov 7271	. 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
2		df-br 5079	. . . 4 ⊢ (𝐴dom 𝐹 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ dom 𝐹)
3		ovprc1.1	. . . . 5 ⊢ Rel dom 𝐹
4	3	brrelex12i 5641	. . . 4 ⊢ (𝐴dom 𝐹 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
5	2, 4	sylbir 234	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom 𝐹 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
6		ndmfv 6798	. . 3 ⊢ (¬ ⟨𝐴, 𝐵⟩ ∈ dom 𝐹 → (𝐹‘⟨𝐴, 𝐵⟩) = ∅)
7	5, 6	nsyl5 159	. 2 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐹‘⟨𝐴, 𝐵⟩) = ∅)
8	1, 7	eqtrid 2791	1 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2109  Vcvv 3430  ∅c0 4261  ⟨cop 4572   class class class wbr 5078  dom cdm 5588  Rel wrel 5593  ‘cfv 6430  (class class class)co 7268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-xp 5594  df-rel 5595  df-dm 5598  df-iota 6388  df-fv 6438  df-ov 7271

This theorem is referenced by:  ovprc1  7307  ovprc2  7308  ovrcl  7309  elbasov  16900  firest  17124  psrplusg  21131  psrmulr  21134  psrvscafval  21140  mplval  21178  opsrle  21229  opsrbaslem  21231  opsrbaslemOLD  21232  evlval  21286  matbas0pc  21537  mdetfval  21716  madufval  21767  mdegfval  25208  nbgrprc0  27682  gonan0  33333  brovmptimex  41590