![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > dif1o | Structured version Unicode version |
Description: Two ways to say that ![]() ![]() |
Ref | Expression |
---|---|
dif1o |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df1o2 7032 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | difeq2i 3569 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | eleq2i 2529 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | eldifsn 4098 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitri 249 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-ral 2800 df-rab 2804 df-v 3070 df-dif 3429 df-un 3431 df-nul 3736 df-sn 3976 df-suc 4823 df-1o 7020 |
This theorem is referenced by: ondif1 7041 brwitnlem 7047 oelim2 7134 oeeulem 7140 oeeui 7141 omabs 7186 cantnfp1lem3 7989 cantnfp1 7990 cantnflem1 7998 cantnflem3 8000 cantnflem4 8001 cantnfleOLD 8010 cantnfp1lem2OLD 8014 cantnfp1lem3OLD 8015 cantnfp1OLD 8016 cantnflem1aOLD 8017 cantnflem1cOLD 8019 cantnflem1OLD 8021 cantnflem3OLD 8022 cantnflem4OLD 8023 cantnfOLD 8024 cnfcom3lem 8037 cnfcomlemOLD 8041 cnfcom3lemOLD 8045 cnfcom3OLD 8046 |
Copyright terms: Public domain | W3C validator |