![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > aovov0bi | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
aovov0bi | ⊢ ((𝐴𝐹𝐵) = ∅ ↔ ( ((𝐴𝐹𝐵)) = ∅ ∨ ((𝐴𝐹𝐵)) = V)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ov 7448 | . . 3 ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | |
2 | 1 | eqeq1i 2739 | . 2 ⊢ ((𝐴𝐹𝐵) = ∅ ↔ (𝐹‘〈𝐴, 𝐵〉) = ∅) |
3 | afvfv0bi 46999 | . 2 ⊢ ((𝐹‘〈𝐴, 𝐵〉) = ∅ ↔ ((𝐹'''〈𝐴, 𝐵〉) = ∅ ∨ (𝐹'''〈𝐴, 𝐵〉) = V)) | |
4 | df-aov 46968 | . . . . 5 ⊢ ((𝐴𝐹𝐵)) = (𝐹'''〈𝐴, 𝐵〉) | |
5 | 4 | eqeq1i 2739 | . . . 4 ⊢ ( ((𝐴𝐹𝐵)) = ∅ ↔ (𝐹'''〈𝐴, 𝐵〉) = ∅) |
6 | 5 | bicomi 224 | . . 3 ⊢ ((𝐹'''〈𝐴, 𝐵〉) = ∅ ↔ ((𝐴𝐹𝐵)) = ∅) |
7 | 4 | eqeq1i 2739 | . . . 4 ⊢ ( ((𝐴𝐹𝐵)) = V ↔ (𝐹'''〈𝐴, 𝐵〉) = V) |
8 | 7 | bicomi 224 | . . 3 ⊢ ((𝐹'''〈𝐴, 𝐵〉) = V ↔ ((𝐴𝐹𝐵)) = V) |
9 | 6, 8 | orbi12i 913 | . 2 ⊢ (((𝐹'''〈𝐴, 𝐵〉) = ∅ ∨ (𝐹'''〈𝐴, 𝐵〉) = V) ↔ ( ((𝐴𝐹𝐵)) = ∅ ∨ ((𝐴𝐹𝐵)) = V)) |
10 | 2, 3, 9 | 3bitri 297 | 1 ⊢ ((𝐴𝐹𝐵) = ∅ ↔ ( ((𝐴𝐹𝐵)) = ∅ ∨ ((𝐴𝐹𝐵)) = V)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∨ wo 846 = wceq 1537 Vcvv 3482 ∅c0 4347 〈cop 4654 ‘cfv 6572 (class class class)co 7445 '''cafv 46964 ((caov 46965 |
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 1967 ax-7 2007 ax-8 2105 ax-9 2113 ax-10 2136 ax-11 2153 ax-12 2173 ax-ext 2705 ax-sep 5320 ax-nul 5327 ax-pr 5450 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2890 df-ne 2943 df-ral 3064 df-rex 3073 df-rab 3439 df-v 3484 df-sbc 3799 df-csb 3916 df-dif 3973 df-un 3975 df-in 3977 df-ss 3987 df-nul 4348 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-int 4973 df-br 5170 df-opab 5232 df-id 5597 df-xp 5705 df-rel 5706 df-cnv 5707 df-co 5708 df-dm 5709 df-res 5711 df-iota 6524 df-fun 6574 df-fv 6580 df-ov 7448 df-aiota 46932 df-dfat 46966 df-afv 46967 df-aov 46968 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |