![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > preq2d | Structured version Unicode version |
Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.) |
Ref | Expression |
---|---|
preq1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
preq2d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | preq1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | preq2 4064 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 16 |
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 1955 ax-ext 2432 |
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 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-v 3080 df-un 3442 df-sn 3987 df-pr 3989 |
This theorem is referenced by: opeq2 4169 opthwiener 4702 fprg 6001 fnprb 6046 opthreg 7936 s2prop 12643 gsumprval 15634 indislem 18737 iscon 19150 hmphindis 19503 wilthlem2 22541 ispth 23620 1pthonlem2 23642 2pthoncl 23655 eupath2lem3 23753 eupath2 23754 measxun2 26770 fprb 27729 altopthsn 28137 wwlknredwwlkn 30507 wwlkextfun 30510 wwlkextinj 30511 wwlkextsur 30512 wwlkextbij 30514 clwwlkn2 30587 clwlkisclwwlklem2a1 30590 clwlkisclwwlklem2a4 30595 clwlkisclwwlklem1 30598 clwwlkf 30605 clwwisshclwwlem1 30618 frgraunss 30736 frgra2v 30740 frgra3v 30743 n4cyclfrgra 30759 extwwlkfablem1 30816 extwwlkfablem2 30820 mapdindp4 35707 |
Copyright terms: Public domain | W3C validator |