![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > fveqvfvv | Structured version Visualization version GIF version |
Description: If a function's value at an argument is the universal class (which can never be the case because of fvex 6506), the function's value at this argument is any set (especially the empty set). In short "If a function's value is a proper class, it is a set", which sounds strange/contradictory, but which is a consequence of that a contradiction implies anything (see pm2.21i 117). (Contributed by Alexander van der Vekens, 26-May-2017.) |
Ref | Expression |
---|---|
fveqvfvv | ⊢ ((𝐹‘𝐴) = V → (𝐹‘𝐴) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvex 6506 | . . . 4 ⊢ (𝐹‘𝐴) ∈ V | |
2 | eleq1a 2855 | . . . 4 ⊢ ((𝐹‘𝐴) ∈ V → (V = (𝐹‘𝐴) → V ∈ V)) | |
3 | 1, 2 | ax-mp 5 | . . 3 ⊢ (V = (𝐹‘𝐴) → V ∈ V) |
4 | vprc 5070 | . . . 4 ⊢ ¬ V ∈ V | |
5 | 4 | pm2.21i 117 | . . 3 ⊢ (V ∈ V → (𝐹‘𝐴) = 𝐵) |
6 | 3, 5 | syl 17 | . 2 ⊢ (V = (𝐹‘𝐴) → (𝐹‘𝐴) = 𝐵) |
7 | 6 | eqcoms 2780 | 1 ⊢ ((𝐹‘𝐴) = V → (𝐹‘𝐴) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2048 Vcvv 3409 ‘cfv 6182 |
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-ext 2745 ax-sep 5054 ax-nul 5061 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 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-ral 3087 df-rex 3088 df-v 3411 df-sbc 3678 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-sn 4436 df-pr 4438 df-uni 4707 df-iota 6146 df-fv 6190 |
This theorem is referenced by: afvpcfv0 42697 |
Copyright terms: Public domain | W3C validator |