New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > pw1eq | Unicode version |
Description: Equality theorem for unit power class. (Contributed by SF, 12-Jan-2015.) |
Ref | Expression |
---|---|
pw1eq | 1 1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pweq 3725 | . . 3 | |
2 | 1 | ineq1d 3456 | . 2 1c 1c |
3 | df-pw1 4137 | . 2 1 1c | |
4 | df-pw1 4137 | . 2 1 1c | |
5 | 2, 3, 4 | 3eqtr4g 2410 | 1 1 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1642 cin 3208 cpw 3722 1cc1c 4134 1 cpw1 4135 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-v 2861 df-nin 3211 df-compl 3212 df-in 3213 df-ss 3259 df-pw 3724 df-pw1 4137 |
This theorem is referenced by: pw10b 4166 pw1equn 4331 pw1eqadj 4332 sspw1 4335 sspw12 4336 addceq2 4384 ncfinraise 4481 ncfinlower 4483 nnpw1ex 4484 tfindi 4496 tfinsuc 4498 sfin01 4528 sfindbl 4530 1cvsfin 4542 vfinspsslem1 4550 rnsi 5521 pw1fnval 5851 pw1fnf1o 5855 enpw1 6062 ncpw1c 6154 ncspw1eu 6159 pw1eltc 6162 tcdi 6164 ce0nnul 6177 ce0nnuli 6178 ce0addcnnul 6179 cenc 6181 ce0nulnc 6184 ce2 6192 elcan 6329 |
Copyright terms: Public domain | W3C validator |