![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > weeq1 | Structured version Visualization version Unicode version |
Description: Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.) |
Ref | Expression |
---|---|
weeq1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | freq1 4804 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | soeq1 4774 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | anbi12d 717 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-we 4795 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | df-we 4795 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3bitr4g 292 |
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 1669 ax-4 1682 ax-5 1758 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-ex 1664 df-cleq 2444 df-clel 2447 df-ral 2742 df-rex 2743 df-br 4403 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 |
This theorem is referenced by: oieq1 8027 hartogslem1 8057 wemapwe 8202 infxpenlem 8444 dfac8b 8462 ac10ct 8465 fpwwe2cbv 9055 fpwwe2lem2 9057 fpwwe2lem5 9059 fpwwecbv 9069 fpwwelem 9070 canthnumlem 9073 canthwelem 9075 canthwe 9076 canthp1lem2 9078 pwfseqlem4a 9086 pwfseqlem4 9087 ltbwe 18696 vitali 22571 fin2so 31932 weeq12d 35898 dnwech 35906 aomclem5 35916 aomclem6 35917 aomclem7 35918 |
Copyright terms: Public domain | W3C validator |