![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > risset | Unicode version |
Description: Two ways to say
"![]() ![]() |
Ref | Expression |
---|---|
risset |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exancom 1586 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-rex 2620 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | df-clel 2349 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | 3bitr4ri 269 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-clel 2349 df-rex 2620 |
This theorem is referenced by: reueq 3033 reuind 3039 0el 3566 iunid 4021 snelpw1 4146 unipw1 4325 addcid1 4405 nncaddccl 4419 vfinspsslem1 4550 vfinspclt 4552 nulnnn 4556 dfproj12 4576 dfproj22 4577 proj1op 4600 proj2op 4601 phidisjnn 4615 phialllem1 4616 dfdm4 5507 dfrn5 5508 oqelins4 5794 otsnelsi3 5805 addcfnex 5824 funsex 5828 qsid 5990 mapexi 6003 xpassen 6057 enpw1lem1 6061 enmap2lem1 6063 enmap1lem1 6069 ovcelem1 6171 ce0nn 6180 finnc 6243 nncdiv3lem1 6275 nchoicelem11 6299 nchoicelem12 6300 nchoicelem17 6305 nchoicelem18 6306 |
Copyright terms: Public domain | W3C validator |