![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > enrefg | Structured version Visualization version GIF version |
Description: Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 18-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
enrefg | ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oi 6287 | . . 3 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 | |
2 | f1oen2g 8089 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴) → 𝐴 ≈ 𝐴) | |
3 | 1, 2 | mp3an3 1526 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ 𝐴) |
4 | 3 | anidms 680 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2103 class class class wbr 4760 I cid 5127 ↾ cres 5220 –1-1-onto→wf1o 6000 ≈ cen 8069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1835 ax-4 1850 ax-5 1952 ax-6 2018 ax-7 2054 ax-8 2105 ax-9 2112 ax-10 2132 ax-11 2147 ax-12 2160 ax-13 2355 ax-ext 2704 ax-sep 4889 ax-nul 4897 ax-pow 4948 ax-pr 5011 ax-un 7066 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1599 df-ex 1818 df-nf 1823 df-sb 2011 df-eu 2575 df-mo 2576 df-clab 2711 df-cleq 2717 df-clel 2720 df-nfc 2855 df-ral 3019 df-rex 3020 df-rab 3023 df-v 3306 df-dif 3683 df-un 3685 df-in 3687 df-ss 3694 df-nul 4024 df-if 4195 df-pw 4268 df-sn 4286 df-pr 4288 df-op 4292 df-uni 4545 df-br 4761 df-opab 4821 df-id 5128 df-xp 5224 df-rel 5225 df-cnv 5226 df-co 5227 df-dm 5228 df-rn 5229 df-res 5230 df-ima 5231 df-fun 6003 df-fn 6004 df-f 6005 df-f1 6006 df-fo 6007 df-f1o 6008 df-en 8073 |
This theorem is referenced by: enref 8105 eqeng 8106 domrefg 8107 difsnen 8158 sdomirr 8213 mapdom1 8241 mapdom2 8247 onfin 8267 ssnnfi 8295 rneqdmfinf1o 8358 infdifsn 8667 infdiffi 8668 onenon 8888 cardonle 8896 cda1en 9110 xpcdaen 9118 mapcdaen 9119 onacda 9132 ssfin4 9245 canthp1lem1 9587 gchhar 9614 hashfac 13355 mreexexlem3d 16429 cyggenod 18407 fidomndrnglem 19429 mdetunilem8 20548 frlmpwfi 38087 fiuneneq 38194 enrelmap 38710 |
Copyright terms: Public domain | W3C validator |