| 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 4514 |
. 2
| |
| 3 | 1, 2 | ax-mp 7 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: domen 4518 ener 4549 en0 4562 ensn1 4563 en1 4565 ac6sfi 4589 canth2 4627 mapen 4636 ssenen 4649 phplem4 4656 php3 4660 ssfi 4681 unfilem3 4694 unifi 4699 fiint 4701 fodomfi 4707 numth2 4929 ruc 7759 infxpidmlem10 7771 infxpidmlem12 7773 infmap2lem1 7789 eqindhome 11007 fbssint 11521 fcluscomplem 11623 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 997 ax-gen 998 ax-8 999 ax-10 1001 ax-11 1002 ax-12 1003 ax-13 1004 ax-14 1005 ax-17 1006 ax-4 1008 ax-5o 1010 ax-6o 1013 ax-9o 1158 ax-10o 1176 ax-16 1246 ax-11o 1254 ax-ext 1499 ax-sep 2776 ax-pow 2817 ax-pr 2854 ax-un 3088 |
| This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-ex 1016 df-sb 1208 df-eu 1420 df-mo 1421 df-clab 1505 df-cleq 1510 df-clel 1513 df-ne 1629 df-v 1857 df-dif 2100 df-un 2101 df-in 2102 df-ss 2104 df-nul 2332 df-pw 2458 df-sn 2469 df-pr 2470 df-op 2473 df-uni 2569 df-br 2692 df-opab 2740 df-xp 3264 df-rel 3265 df-cnv 3266 df-dm 3268 df-rn 3269 df-fn 3273 df-f 3274 df-f1 3275 df-fo 3276 df-f1o 3277 df-en 4507 |