![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > aov0nbovbi | Structured version Visualization version GIF version |
Description: The operation's value on an ordered pair is an element of a set if and only if the alternative value of the operation on this ordered pair is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.) |
Ref | Expression |
---|---|
aov0nbovbi | ⊢ (∅ ∉ 𝐶 → ( ((𝐴𝐹𝐵)) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | afv0nbfvbi 42052 | . 2 ⊢ (∅ ∉ 𝐶 → ((𝐹'''〈𝐴, 𝐵〉) ∈ 𝐶 ↔ (𝐹‘〈𝐴, 𝐵〉) ∈ 𝐶)) | |
2 | df-aov 42022 | . . 3 ⊢ ((𝐴𝐹𝐵)) = (𝐹'''〈𝐴, 𝐵〉) | |
3 | 2 | eleq1i 2896 | . 2 ⊢ ( ((𝐴𝐹𝐵)) ∈ 𝐶 ↔ (𝐹'''〈𝐴, 𝐵〉) ∈ 𝐶) |
4 | df-ov 6907 | . . 3 ⊢ (𝐴𝐹𝐵) = (𝐹‘〈𝐴, 𝐵〉) | |
5 | 4 | eleq1i 2896 | . 2 ⊢ ((𝐴𝐹𝐵) ∈ 𝐶 ↔ (𝐹‘〈𝐴, 𝐵〉) ∈ 𝐶) |
6 | 1, 3, 5 | 3bitr4g 306 | 1 ⊢ (∅ ∉ 𝐶 → ( ((𝐴𝐹𝐵)) ∈ 𝐶 ↔ (𝐴𝐹𝐵) ∈ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∈ wcel 2166 ∉ wnel 3101 ∅c0 4143 〈cop 4402 ‘cfv 6122 (class class class)co 6904 '''cafv 42018 ((caov 42019 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-sep 5004 ax-nul 5012 ax-pow 5064 ax-pr 5126 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-fal 1672 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ne 2999 df-nel 3102 df-ral 3121 df-rex 3122 df-rab 3125 df-v 3415 df-sbc 3662 df-csb 3757 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-int 4697 df-br 4873 df-opab 4935 df-id 5249 df-xp 5347 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-res 5353 df-iota 6085 df-fun 6124 df-fv 6130 df-ov 6907 df-aiota 41981 df-dfat 42020 df-afv 42021 df-aov 42022 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |