This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐵