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

Metamath Proof Explorer

Theorem iunssfOLD

Description: Obsolete version of iunssf as of 2-Feb-2026. (Contributed by Glauco Siliprandi, 3-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis iunssf.1 ⊢ Ⅎ _ x C
Assertion iunssfOLD ⊢ ⋃ x ∈ A B ⊆ C ↔ ∀ x ∈ A B ⊆ C

Proof

Step Hyp Ref Expression
1 iunssf.1 ⊢ Ⅎ _ x C
2 df-iun ⊢ ⋃ x ∈ A B = y | ∃ x ∈ A y ∈ B
3 2 sseq1i ⊢ ⋃ x ∈ A B ⊆ C ↔ y | ∃ x ∈ A y ∈ B ⊆ C
4 abss ⊢ y | ∃ x ∈ A y ∈ B ⊆ C ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ C
5 df-ss ⊢ B ⊆ C ↔ ∀ y y ∈ B → y ∈ C
6 5 ralbii ⊢ ∀ x ∈ A B ⊆ C ↔ ∀ x ∈ A ∀ y y ∈ B → y ∈ C
7 ralcom4 ⊢ ∀ x ∈ A ∀ y y ∈ B → y ∈ C ↔ ∀ y ∀ x ∈ A y ∈ B → y ∈ C
8 1 nfcri ⊢ Ⅎ x y ∈ C
9 8 r19.23 ⊢ ∀ x ∈ A y ∈ B → y ∈ C ↔ ∃ x ∈ A y ∈ B → y ∈ C
10 9 albii ⊢ ∀ y ∀ x ∈ A y ∈ B → y ∈ C ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ C
11 6 7 10 3bitrri ⊢ ∀ y ∃ x ∈ A y ∈ B → y ∈ C ↔ ∀ x ∈ A B ⊆ C
12 3 4 11 3bitri ⊢ ⋃ x ∈ A B ⊆ C ↔ ∀ x ∈ A B ⊆ C