Theorem bnj1146

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	bnj1146.1	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
Assertion	bnj1146	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵

Proof

Step	Hyp	Ref	Expression
1		bnj1146.1	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
2		nfv	⊢ Ⅎ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 )
3	1	nf5i	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐴
4		nfv	⊢ Ⅎ 𝑥 𝑤 ∈ 𝐵
5	3 4	nfan	⊢ Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 )
6		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
7	6	anbi1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ) )
8	2 5 7	cbvexv1	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) )
9		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) )
10		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵 ) )
11	8 9 10	3bitr4i	⊢ ( ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 ↔ ∃ 𝑦 ∈ 𝐴 𝑤 ∈ 𝐵 )
12	11	abbii	⊢ { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 } = { 𝑤 ∣ ∃ 𝑦 ∈ 𝐴 𝑤 ∈ 𝐵 }
13		df-iun	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = { 𝑤 ∣ ∃ 𝑥 ∈ 𝐴 𝑤 ∈ 𝐵 }
14		df-iun	⊢ ∪ 𝑦 ∈ 𝐴 𝐵 = { 𝑤 ∣ ∃ 𝑦 ∈ 𝐴 𝑤 ∈ 𝐵 }
15	12 13 14	3eqtr4i	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐵
16		bnj1143	⊢ ∪ 𝑦 ∈ 𝐴 𝐵 ⊆ 𝐵
17	15 16	eqsstri	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵