Theorem aovov0bi 47157

Description: The operation's value on an ordered pair is the empty set if and only if the alternative value of the operation on this ordered pair is either the empty set or the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.)

Assertion

Ref	Expression
aovov0bi	⊢ ((𝐴𝐹𝐵) = ∅ ↔ ( ((𝐴𝐹𝐵)) = ∅ ∨ ((𝐴𝐹𝐵)) = V))

Proof of Theorem aovov0bi

Step	Hyp	Ref	Expression
1		df-ov 7438	. . 3 ⊢ (𝐴𝐹𝐵) = (𝐹‘⟨𝐴, 𝐵⟩)
2	1	eqeq1i 2741	. 2 ⊢ ((𝐴𝐹𝐵) = ∅ ↔ (𝐹‘⟨𝐴, 𝐵⟩) = ∅)
3		afvfv0bi 47113	. 2 ⊢ ((𝐹‘⟨𝐴, 𝐵⟩) = ∅ ↔ ((𝐹'''⟨𝐴, 𝐵⟩) = ∅ ∨ (𝐹'''⟨𝐴, 𝐵⟩) = V))
4		df-aov 47082	. . . . 5 ⊢ ((𝐴𝐹𝐵)) = (𝐹'''⟨𝐴, 𝐵⟩)
5	4	eqeq1i 2741	. . . 4 ⊢ ( ((𝐴𝐹𝐵)) = ∅ ↔ (𝐹'''⟨𝐴, 𝐵⟩) = ∅)
6	5	bicomi 224	. . 3 ⊢ ((𝐹'''⟨𝐴, 𝐵⟩) = ∅ ↔ ((𝐴𝐹𝐵)) = ∅)
7	4	eqeq1i 2741	. . . 4 ⊢ ( ((𝐴𝐹𝐵)) = V ↔ (𝐹'''⟨𝐴, 𝐵⟩) = V)
8	7	bicomi 224	. . 3 ⊢ ((𝐹'''⟨𝐴, 𝐵⟩) = V ↔ ((𝐴𝐹𝐵)) = V)
9	6, 8	orbi12i 914	. 2 ⊢ (((𝐹'''⟨𝐴, 𝐵⟩) = ∅ ∨ (𝐹'''⟨𝐴, 𝐵⟩) = V) ↔ ( ((𝐴𝐹𝐵)) = ∅ ∨ ((𝐴𝐹𝐵)) = V))
10	2, 3, 9	3bitri 297	1 ⊢ ((𝐴𝐹𝐵) = ∅ ↔ ( ((𝐴𝐹𝐵)) = ∅ ∨ ((𝐴𝐹𝐵)) = V))

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1538  Vcvv 3479  ∅c0 4340  ⟨cop 4638  ‘cfv 6566  (class class class)co 7435  '''cafv 47078   ((caov 47079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  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 2707  ax-sep 5303  ax-nul 5313  ax-pr 5439

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1778  df-nf 1782  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3435  df-v 3481  df-sbc 3793  df-csb 3910  df-dif 3967  df-un 3969  df-in 3971  df-ss 3981  df-nul 4341  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4914  df-int 4953  df-br 5150  df-opab 5212  df-id 5584  df-xp 5696  df-rel 5697  df-cnv 5698  df-co 5699  df-dm 5700  df-res 5702  df-iota 6519  df-fun 6568  df-fv 6574  df-ov 7438  df-aiota 47046  df-dfat 47080  df-afv 47081  df-aov 47082

This theorem is referenced by: (None)