Metamath Proof Explorer


Theorem intmin2

Description: Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003)

Ref Expression
Hypothesis intmin2.1 AV
Assertion intmin2 x|Ax=A

Proof

Step Hyp Ref Expression
1 intmin2.1 AV
2 rabab xV|Ax=x|Ax
3 2 inteqi xV|Ax=x|Ax
4 intmin AVxV|Ax=A
5 1 4 ax-mp xV|Ax=A
6 3 5 eqtr3i x|Ax=A