Metamath Proof Explorer


Theorem intmin

Description: Any member of a class is the smallest of those members that include it. (Contributed by NM, 13-Aug-2002) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion intmin ( 𝐴𝐵 { 𝑥𝐵𝐴𝑥 } = 𝐴 )

Proof

Step Hyp Ref Expression
1 vex 𝑦 ∈ V
2 1 elintrab ( 𝑦 { 𝑥𝐵𝐴𝑥 } ↔ ∀ 𝑥𝐵 ( 𝐴𝑥𝑦𝑥 ) )
3 ssid 𝐴𝐴
4 sseq2 ( 𝑥 = 𝐴 → ( 𝐴𝑥𝐴𝐴 ) )
5 eleq2 ( 𝑥 = 𝐴 → ( 𝑦𝑥𝑦𝐴 ) )
6 4 5 imbi12d ( 𝑥 = 𝐴 → ( ( 𝐴𝑥𝑦𝑥 ) ↔ ( 𝐴𝐴𝑦𝐴 ) ) )
7 6 rspcv ( 𝐴𝐵 → ( ∀ 𝑥𝐵 ( 𝐴𝑥𝑦𝑥 ) → ( 𝐴𝐴𝑦𝐴 ) ) )
8 3 7 mpii ( 𝐴𝐵 → ( ∀ 𝑥𝐵 ( 𝐴𝑥𝑦𝑥 ) → 𝑦𝐴 ) )
9 2 8 syl5bi ( 𝐴𝐵 → ( 𝑦 { 𝑥𝐵𝐴𝑥 } → 𝑦𝐴 ) )
10 9 ssrdv ( 𝐴𝐵 { 𝑥𝐵𝐴𝑥 } ⊆ 𝐴 )
11 ssintub 𝐴 { 𝑥𝐵𝐴𝑥 }
12 11 a1i ( 𝐴𝐵𝐴 { 𝑥𝐵𝐴𝑥 } )
13 10 12 eqssd ( 𝐴𝐵 { 𝑥𝐵𝐴𝑥 } = 𝐴 )