![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ndmfv | Structured version Visualization version GIF version |
Description: The value of a class outside its domain is the empty set. (An artifact of our function value definition.) (Contributed by NM, 24-Aug-1995.) |
Ref | Expression |
---|---|
ndmfv | ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | euex 2637 | . . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 → ∃𝑥 𝐴𝐹𝑥) | |
2 | eldmg 5731 | . . . . 5 ⊢ (𝐴 ∈ V → (𝐴 ∈ dom 𝐹 ↔ ∃𝑥 𝐴𝐹𝑥)) | |
3 | 1, 2 | syl5ibr 249 | . . . 4 ⊢ (𝐴 ∈ V → (∃!𝑥 𝐴𝐹𝑥 → 𝐴 ∈ dom 𝐹)) |
4 | 3 | con3d 155 | . . 3 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → ¬ ∃!𝑥 𝐴𝐹𝑥)) |
5 | tz6.12-2 6635 | . . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅) | |
6 | 4, 5 | syl6 35 | . 2 ⊢ (𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)) |
7 | fvprc 6638 | . . 3 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅) | |
8 | 7 | a1d 25 | . 2 ⊢ (¬ 𝐴 ∈ V → (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅)) |
9 | 6, 8 | pm2.61i 185 | 1 ⊢ (¬ 𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1538 ∃wex 1781 ∈ wcel 2111 ∃!weu 2628 Vcvv 3441 ∅c0 4243 class class class wbr 5030 dom cdm 5519 ‘cfv 6324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-nul 5174 ax-pow 5231 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-dm 5529 df-iota 6283 df-fv 6332 |
This theorem is referenced by: ndmfvrcl 6676 elfvdm 6677 nfvres 6681 fvfundmfvn0 6683 0fv 6684 funfv 6725 fvun1 6729 fvco4i 6739 fvmpti 6744 mptrcl 6754 fvmptss 6757 fvmptex 6759 fvmptnf 6767 fvmptss2 6770 elfvmptrab1 6772 fvopab4ndm 6774 f0cli 6841 funiunfv 6985 ovprc 7173 oprssdm 7309 nssdmovg 7310 ndmovg 7311 1st2val 7699 2nd2val 7700 brovpreldm 7767 smofvon2 7976 rdgsucmptnf 8048 frsucmptn 8057 brwitnlem 8115 undifixp 8481 r1tr 9189 rankvaln 9212 cardidm 9372 carden2a 9379 carden2b 9380 carddomi2 9383 sdomsdomcardi 9384 pm54.43lem 9413 alephcard 9481 alephnbtwn 9482 alephgeom 9493 cfub 9660 cardcf 9663 cflecard 9664 cfle 9665 cflim2 9674 cfidm 9686 itunisuc 9830 itunitc1 9831 ituniiun 9833 alephadd 9988 alephreg 9993 pwcfsdom 9994 cfpwsdom 9995 adderpq 10367 mulerpq 10368 uzssz 12252 ltweuz 13324 wrdsymb0 13892 lsw0 13908 swrd00 13997 swrd0 14011 pfx00 14027 pfx0 14028 sumz 15071 sumss 15073 sumnul 15107 prod1 15290 prodss 15293 divsfval 16812 cidpropd 16972 lubval 17586 glbval 17599 joinval 17607 meetval 17621 gsumpropd2lem 17881 mulgfval 18218 mpfrcl 20757 iscnp2 21844 setsmstopn 23085 tngtopn 23256 dvbsss 24505 perfdvf 24506 dchrrcl 25824 structiedg0val 26815 snstriedgval 26831 rgrx0nd 27384 vsfval 28416 dmadjrnb 29689 hmdmadj 29723 funeldmb 33119 rdgprc0 33151 soseq 33209 nofv 33277 sltres 33282 noseponlem 33284 noextenddif 33288 noextendlt 33289 noextendgt 33290 nolesgn2ores 33292 fvnobday 33296 nosepdmlem 33300 nosepssdm 33303 nosupbnd1lem3 33323 nosupbnd1lem5 33325 nosupbnd2lem1 33328 fullfunfv 33521 linedegen 33717 bj-inftyexpitaudisj 34620 bj-inftyexpidisj 34625 bj-fvimacnv0 34701 dibvalrel 38459 dicvalrelN 38481 dihvalrel 38575 itgocn 40108 r1rankcld 40939 grur1cld 40940 uz0 42049 climfveq 42311 climfveqf 42322 afv2ndeffv0 43816 fvmptrabdm 43849 |
Copyright terms: Public domain | W3C validator |