![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > aov0ov0 | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
aov0ov0 | ⊢ ( ((𝐴𝐹𝐵)) = ∅ → (𝐴𝐹𝐵) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | afv0fv0 44058 | . 2 ⊢ ((𝐹'''〈𝐴, 𝐵〉) = ∅ → (𝐹‘〈𝐴, 𝐵〉) = ∅) | |
2 | df-aov 44030 | . . 3 ⊢ ((𝐴𝐹𝐵)) = (𝐹'''〈𝐴, 𝐵〉) | |
3 | 2 | eqeq1i 2764 | . 2 ⊢ ( ((𝐴𝐹𝐵)) = ∅ ↔ (𝐹'''〈𝐴, 𝐵〉) = ∅) |
4 | df-ov 7146 | . . 3 ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | |
5 | 4 | eqeq1i 2764 | . 2 ⊢ ((𝐴𝐹𝐵) = ∅ ↔ (𝐹‘〈𝐴, 𝐵〉) = ∅) |
6 | 1, 3, 5 | 3imtr4i 296 | 1 ⊢ ( ((𝐴𝐹𝐵)) = ∅ → (𝐴𝐹𝐵) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∅c0 4221 〈cop 4521 ‘cfv 6328 (class class class)co 7143 '''cafv 44026 ((caov 44027 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-ral 3073 df-rex 3074 df-rab 3077 df-v 3409 df-sbc 3694 df-csb 3802 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-nul 4222 df-if 4414 df-sn 4516 df-pr 4518 df-op 4522 df-uni 4792 df-int 4832 df-br 5026 df-opab 5088 df-id 5423 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-res 5529 df-iota 6287 df-fun 6330 df-fv 6336 df-ov 7146 df-aiota 43993 df-dfat 44028 df-afv 44029 df-aov 44030 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |