Metamath Proof Explorer

Theorem reliunOLD

Description: Obsolete version of reliun as of 2-Feb-2025. (Contributed by NM, 19-Dec-2008) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion reliunOLD ⊢ Rel ⁡ ⋃ x ∈ A B ↔ ∀ x ∈ A Rel ⁡ B

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ⋃ x ∈ A B = y | ∃ x ∈ A y ∈ B
2 1 releqi ⊢ Rel ⁡ ⋃ x ∈ A B ↔ Rel ⁡ y | ∃ x ∈ A y ∈ B
3 df-rel ⊢ Rel ⁡ y | ∃ x ∈ A y ∈ B ↔ y | ∃ x ∈ A y ∈ B ⊆ V × V
4 abss ⊢ y | ∃ x ∈ A y ∈ B ⊆ V × V ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ V × V
5 df-rel ⊢ Rel ⁡ B ↔ B ⊆ V × V
6 df-ss ⊢ B ⊆ V × V ↔ ∀ y y ∈ B → y ∈ V × V
7 5 6 bitri ⊢ Rel ⁡ B ↔ ∀ y y ∈ B → y ∈ V × V
8 7 ralbii ⊢ ∀ x ∈ A Rel ⁡ B ↔ ∀ x ∈ A ∀ y y ∈ B → y ∈ V × V
9 ralcom4 ⊢ ∀ x ∈ A ∀ y y ∈ B → y ∈ V × V ↔ ∀ y ∀ x ∈ A y ∈ B → y ∈ V × V
10 r19.23v ⊢ ∀ x ∈ A y ∈ B → y ∈ V × V ↔ ∃ x ∈ A y ∈ B → y ∈ V × V
11 10 albii ⊢ ∀ y ∀ x ∈ A y ∈ B → y ∈ V × V ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ V × V
12 8 9 11 3bitri ⊢ ∀ x ∈ A Rel ⁡ B ↔ ∀ y ∃ x ∈ A y ∈ B → y ∈ V × V
13 4 12 bitr4i ⊢ y | ∃ x ∈ A y ∈ B ⊆ V × V ↔ ∀ x ∈ A Rel ⁡ B
14 2 3 13 3bitri ⊢ Rel ⁡ ⋃ x ∈ A B ↔ ∀ x ∈ A Rel ⁡ B