| 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 6810 | . . 3 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴 | |
| 2 | f1oen2g 8906 | . . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ∧ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴) → 𝐴 ≈ 𝐴) | |
| 3 | 1, 2 | mp3an3 1453 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → 𝐴 ≈ 𝐴) |
| 4 | 3 | anidms 566 | 1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2114 class class class wbr 5086 I cid 5516 ↾ cres 5624 –1-1-onto→wf1o 6489 ≈ cen 8881 |
| 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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-sep 5231 ax-pow 5300 ax-pr 5368 ax-un 7680 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-ral 3053 df-rex 3063 df-rab 3391 df-v 3432 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-opab 5149 df-id 5517 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-en 8885 |
| This theorem is referenced by: enref 8923 eqeng 8924 domrefg 8925 difsnen 8988 sdomirr 9043 mapdom1 9071 mapdom2 9077 rneqdmfinf1o 9234 infdifsn 9567 infdiffi 9568 onenon 9862 cardonle 9870 dju1en 10083 xpdjuen 10091 mapdjuen 10092 onadju 10105 nnadju 10109 ssfin4 10221 canthp1lem1 10564 gchhar 10591 hashfac 14409 mreexexlem3d 17601 cyggenod 19848 mdetunilem8 22593 frlmpwfi 43541 fiuneneq 43635 enrelmap 44439 |
| Copyright terms: Public domain | W3C validator |