Theorem ovprc 7398

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 7363	. 2 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
2		df-br 5087	. . . 4 ⊢ (𝐴dom 𝐹 𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ dom 𝐹)
3		ovprc1.1	. . . . 5 ⊢ Rel dom 𝐹
4	3	brrelex12i 5679	. . . 4 ⊢ (𝐴dom 𝐹 𝐵 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
5	2, 4	sylbir 235	. . 3 ⊢ (⟨𝐴, 𝐵⟩ ∈ dom 𝐹 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
6		ndmfv 6866	. . 3 ⊢ (¬ ⟨𝐴, 𝐵⟩ ∈ dom 𝐹 → (𝐹‘⟨𝐴, 𝐵⟩) = ∅)
7	5, 6	nsyl5 159	. 2 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐹‘⟨𝐴, 𝐵⟩) = ∅)
8	1, 7	eqtrid 2784	1 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3430  ∅c0 4274  ⟨cop 4574   class class class wbr 5086  dom cdm 5624  Rel wrel 5629  ‘cfv 6492  (class class class)co 7360

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 5370

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 5630  df-rel 5631  df-dm 5634  df-iota 6448  df-fv 6500  df-ov 7363

This theorem is referenced by:  ovprc1  7399  ovprc2  7400  ovrcl  7401  elbasov  17177  firest  17386  psrplusg  21926  psrmulr  21931  psrvscafval  21937  mplval  21977  opsrle  22035  opsrbaslem  22037  evlval  22088  matbas0pc  22384  mdetfval  22561  madufval  22612  mdegfval  26037  nbgrprc0  29417  gonan0  35590  brovmptimex  44472  clnbgrprc0  48308  gricrcl  48402  grlicrcl  48495  grilcbri2  48499  upfval  49663  reldmprcof1  49868  reldmprcof2  49869  lmdfval  50136  cmdfval  50137