Metamath Proof Explorer

Theorem unissbOLD

Description: Obsolete version of unissb as of 28-Dec-2024. (Contributed by NM, 20-Sep-2003) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion unissbOLD ( ∪ 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 eluni ⊢ ( 𝑦 ∈ ∪ 𝐴 ↔ ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) )
2 1 imbi1i ⊢ ( ( 𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵 ) ↔ ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
3 19.23v ⊢ ( ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ( ∃ 𝑥 ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
4 2 3 bitr4i ⊢ ( ( 𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
5 4 albii ⊢ ( ∀ 𝑦 ( 𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
6 alcom ⊢ ( ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) )
7 19.21v ⊢ ( ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) )
8 impexp ⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) ) )
9 bi2.04 ⊢ ( ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) )
10 8 9 bitri ⊢ ( ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) )
11 10 albii ⊢ ( ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑦 ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) )
12 df-ss ⊢ ( 𝑥 ⊆ 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) )
13 12 imbi2i ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝐵 ) ) )
14 7 11 13 3bitr4i ⊢ ( ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) )
15 14 albii ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) )
16 6 15 bitri ⊢ ( ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) )
17 5 16 bitri ⊢ ( ∀ 𝑦 ( 𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) )
18 df-ss ⊢ ( ∪ 𝐴 ⊆ 𝐵 ↔ ∀ 𝑦 ( 𝑦 ∈ ∪ 𝐴 → 𝑦 ∈ 𝐵 ) )
19 df-ral ⊢ ( ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐵 ) )
20 17 18 19 3bitr4i ⊢ ( ∪ 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ⊆ 𝐵 )