Metamath Proof Explorer

Theorem rabfmpunirn

Description: Membership in a union of a mapping function-defined family of sets. (Contributed by Thierry Arnoux, 30-Sep-2016)

Ref Expression
Hypotheses rabfmpunirn.1 ⊢ F = x ∈ V ⟼ y ∈ W | φ
rabfmpunirn.2 ⊢ W ∈ V
rabfmpunirn.3 ⊢ y = B → φ ↔ ψ
Assertion rabfmpunirn ⊢ B ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ V B ∈ W ∧ ψ

Proof

Step Hyp Ref Expression
1 rabfmpunirn.1 ⊢ F = x ∈ V ⟼ y ∈ W | φ
2 rabfmpunirn.2 ⊢ W ∈ V
3 rabfmpunirn.3 ⊢ y = B → φ ↔ ψ
4 df-rab ⊢ y ∈ W | φ = y | y ∈ W ∧ φ
5 4 mpteq2i ⊢ x ∈ V ⟼ y ∈ W | φ = x ∈ V ⟼ y | y ∈ W ∧ φ
6 1 5 eqtri ⊢ F = x ∈ V ⟼ y | y ∈ W ∧ φ
7 sepab ⊢ W ∈ V → y | y ∈ W ∧ φ ∈ V
8 2 7 ax-mp ⊢ y | y ∈ W ∧ φ ∈ V
9 eleq1 ⊢ y = B → y ∈ W ↔ B ∈ W
10 9 3 anbi12d ⊢ y = B → y ∈ W ∧ φ ↔ B ∈ W ∧ ψ
11 6 8 10 abfmpunirn ⊢ B ∈ ⋃ ran ⁡ F ↔ B ∈ V ∧ ∃ x ∈ V B ∈ W ∧ ψ
12 elex ⊢ B ∈ W → B ∈ V
13 12 adantr ⊢ B ∈ W ∧ ψ → B ∈ V
14 13 rexlimivw ⊢ ∃ x ∈ V B ∈ W ∧ ψ → B ∈ V
15 14 pm4.71ri ⊢ ∃ x ∈ V B ∈ W ∧ ψ ↔ B ∈ V ∧ ∃ x ∈ V B ∈ W ∧ ψ
16 11 15 bitr4i ⊢ B ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ V B ∈ W ∧ ψ