| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Equinumerosity relation. Compare Definition of [Enderton] p. 129. |
| Ref | Expression |
|---|---|
| bren.1 |
|
| Ref | Expression |
|---|---|
| bren |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bren.1 |
. 2
| |
| 2 | breng 4363 |
. 2
| |
| 3 | 1, 2 | ax-mp 7 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: domen 4367 ener 4397 en0 4410 ensn1 4411 en1 4413 canth2 4470 mapen 4477 ssenen 4490 phplem4 4497 php3 4501 ssfi 4521 unfilem3 4532 unifi 4538 fiint 4540 fodomfi 4546 numth2 4765 ruc 7500 infxpidmlem10 7512 infxpidmlem12 7514 infmap2lem1 7529 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-sep 2698 ax-pow 2737 ax-pr 2774 ax-un 2861 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-v 1808 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-nul 2277 df-pw 2398 df-sn 2408 df-pr 2409 df-op 2412 df-uni 2499 df-br 2615 df-opab 2662 df-xp 3179 df-rel 3180 df-cnv 3181 df-dm 3183 df-rn 3184 df-fn 3188 df-f 3189 df-f1 3190 df-fo 3191 df-f1o 3192 df-en 4357 |