Theorem aov0ov0 47139

Description: If the alternative value of the operation on an ordered pair is the empty set, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.)

Assertion

Ref	Expression
aov0ov0	⊢ ( ((𝐴𝐹𝐵)) = ∅ → (𝐴𝐹𝐵) = ∅)

Proof of Theorem aov0ov0

Step	Hyp	Ref	Expression
1		afv0fv0 47095	. 2 ⊢ ((𝐹'''⟨𝐴, 𝐵⟩) = ∅ → (𝐹‘⟨𝐴, 𝐵⟩) = ∅)
2		df-aov 47067	. . 3 ⊢ ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)
3	2	eqeq1i 2739	. 2 ⊢ ( ((𝐴𝐹𝐵)) = ∅ ↔ (𝐹'''⟨𝐴, 𝐵⟩) = ∅)
4		df-ov 7415	. . 3 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
5	4	eqeq1i 2739	. 2 ⊢ ((𝐴𝐹𝐵) = ∅ ↔ (𝐹‘⟨𝐴, 𝐵⟩) = ∅)
6	1, 3, 5	3imtr4i 292	1 ⊢ ( ((𝐴𝐹𝐵)) = ∅ → (𝐴𝐹𝐵) = ∅)

Syntax hints:   → wi 4   = wceq 1539  ∅c0 4313  ⟨cop 4612  ‘cfv 6540  (class class class)co 7412  '''cafv 47063   ((caov 47064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-int 4927  df-br 5124  df-opab 5186  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-res 5677  df-iota 6493  df-fun 6542  df-fv 6548  df-ov 7415  df-aiota 47031  df-dfat 47065  df-afv 47066  df-aov 47067

This theorem is referenced by: (None)