Theorem dfuni2

Description: Alternate definition of class union. (Contributed by NM, 28-Jun-1998)

	Ref	Expression
Assertion	dfuni2	⊢ ∪ 𝐴 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 }

Proof

Step	Hyp	Ref	Expression
1		df-uni	⊢ ∪ 𝐴 = { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) }
2		exancom	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) )
3		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦 ) )
4	2 3	bitr4i	⊢ ( ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 )
5	4	abbii	⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝐴 ) } = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 }
6	1 5	eqtri	⊢ ∪ 𝐴 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 }