Theorem unimax

Description: Any member of a class is the largest of those members that it includes. (Contributed by NM, 13-Aug-2002)

	Ref	Expression
Assertion	unimax	⊢ ( 𝐴 ∈ 𝐵 → ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ 𝐴 ⊆ 𝐴
2		sseq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴 ) )
3	2	elrab3	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ↔ 𝐴 ⊆ 𝐴 ) )
4	1 3	mpbiri	⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } )
5		sseq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
6	5	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) )
7	6	simprbi	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } → 𝑦 ⊆ 𝐴 )
8	7	rgen	⊢ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } 𝑦 ⊆ 𝐴
9		ssunieq	⊢ ( ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } 𝑦 ⊆ 𝐴 ) → 𝐴 = ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } )
10	9	eqcomd	⊢ ( ( 𝐴 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ∧ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } 𝑦 ⊆ 𝐴 ) → ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } = 𝐴 )
11	4 8 10	sylancl	⊢ ( 𝐴 ∈ 𝐵 → ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } = 𝐴 )