![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > aovpcov0 | Structured version Visualization version GIF version |
Description: If the alternative value of the operation on an ordered pair is the universal class, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.) |
Ref | Expression |
---|---|
aovpcov0 | ⊢ ( ((𝐴𝐹𝐵)) = V → (𝐴𝐹𝐵) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | afvpcfv0 42697 | . 2 ⊢ ((𝐹'''〈𝐴, 𝐵〉) = V → (𝐹‘〈𝐴, 𝐵〉) = ∅) | |
2 | df-aov 42672 | . . 3 ⊢ ((𝐴𝐹𝐵)) = (𝐹'''〈𝐴, 𝐵〉) | |
3 | 2 | eqeq1i 2777 | . 2 ⊢ ( ((𝐴𝐹𝐵)) = V ↔ (𝐹'''〈𝐴, 𝐵〉) = V) |
4 | df-ov 6973 | . . 3 ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | |
5 | 4 | eqeq1i 2777 | . 2 ⊢ ((𝐴𝐹𝐵) = ∅ ↔ (𝐹‘〈𝐴, 𝐵〉) = ∅) |
6 | 1, 3, 5 | 3imtr4i 284 | 1 ⊢ ( ((𝐴𝐹𝐵)) = V → (𝐴𝐹𝐵) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 Vcvv 3409 ∅c0 4173 〈cop 4441 ‘cfv 6182 (class class class)co 6970 '''cafv 42668 ((caov 42669 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-int 4744 df-br 4924 df-opab 4986 df-id 5305 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-res 5412 df-iota 6146 df-fun 6184 df-fv 6190 df-ov 6973 df-aiota 42637 df-dfat 42670 df-afv 42671 df-aov 42672 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |