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 ⊢ y ∈ A → ∀ x y ∈ A
Assertion bnj1146 ⊢ ⋃ x ∈ A B ⊆ B

Proof

Step Hyp Ref Expression
1 bnj1146.1 ⊢ y ∈ A → ∀ x y ∈ A
2 nfv ⊢ Ⅎ y x ∈ A ∧ w ∈ B
3 1 nf5i ⊢ Ⅎ x y ∈ A
4 nfv ⊢ Ⅎ x w ∈ B
5 3 4 nfan ⊢ Ⅎ x y ∈ A ∧ w ∈ B
6 eleq1w ⊢ x = y → x ∈ A ↔ y ∈ A
7 6 anbi1d ⊢ x = y → x ∈ A ∧ w ∈ B ↔ y ∈ A ∧ w ∈ B
8 2 5 7 cbvexv1 ⊢ ∃ x x ∈ A ∧ w ∈ B ↔ ∃ y y ∈ A ∧ w ∈ B
9 df-rex ⊢ ∃ x ∈ A w ∈ B ↔ ∃ x x ∈ A ∧ w ∈ B
10 df-rex ⊢ ∃ y ∈ A w ∈ B ↔ ∃ y y ∈ A ∧ w ∈ B
11 8 9 10 3bitr4i ⊢ ∃ x ∈ A w ∈ B ↔ ∃ y ∈ A w ∈ B
12 11 abbii ⊢ w | ∃ x ∈ A w ∈ B = w | ∃ y ∈ A w ∈ B
13 df-iun ⊢ ⋃ x ∈ A B = w | ∃ x ∈ A w ∈ B
14 df-iun ⊢ ⋃ y ∈ A B = w | ∃ y ∈ A w ∈ B
15 12 13 14 3eqtr4i ⊢ ⋃ x ∈ A B = ⋃ y ∈ A B
16 bnj1143 ⊢ ⋃ y ∈ A B ⊆ B
17 15 16 eqsstri ⊢ ⋃ x ∈ A B ⊆ B