![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > enref | Structured version Visualization version GIF version |
Description: Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92. (Contributed by NM, 25-Sep-2004.) |
Ref | Expression |
---|---|
enref.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
enref | ⊢ 𝐴 ≈ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | enref.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | enrefg 8394 | . 2 ⊢ (𝐴 ∈ V → 𝐴 ≈ 𝐴) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐴 ≈ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2081 Vcvv 3437 class class class wbr 4966 ≈ cen 8359 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-br 4967 df-opab 5029 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-en 8363 |
This theorem is referenced by: ener 8409 en0 8425 pwen 8542 phplem2 8549 phplem3 8550 isinf 8582 pssnn 8587 karden 9175 mappwen 9389 infmap2 9491 ackbij1lem5 9497 axcc4dom 9714 domtriomlem 9715 cfpwsdom 9857 0tsk 10028 fzennn 13191 qnnen 15404 rpnnen 15418 rexpen 15419 lmisfree 20673 met2ndci 22820 lgseisenlem2 25639 poimirlem9 34457 poimirlem26 34474 |
Copyright terms: Public domain | W3C validator |