Metamath Proof Explorer
Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004)
|
|
Ref |
Expression |
|
Hypotheses |
eleqtrd.1 |
|
|
|
eleqtrd.2 |
|
|
Assertion |
eleqtrd |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
eleqtrd.1 |
|
2 |
|
eleqtrd.2 |
|
3 |
2
|
eleq2d |
|
4 |
1 3
|
mpbid |
|