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 2 zfausab ⊢ y | y ∈ W ∧ φ ∈ V
8 eleq1 ⊢ y = B → y ∈ W ↔ B ∈ W
9 8 3 anbi12d ⊢ y = B → y ∈ W ∧ φ ↔ B ∈ W ∧ ψ
10 6 7 9 abfmpunirn ⊢ B ∈ ⋃ ran ⁡ F ↔ B ∈ V ∧ ∃ x ∈ V B ∈ W ∧ ψ
11 elex ⊢ B ∈ W → B ∈ V
12 11 adantr ⊢ B ∈ W ∧ ψ → B ∈ V
13 12 rexlimivw ⊢ ∃ x ∈ V B ∈ W ∧ ψ → B ∈ V
14 13 pm4.71ri ⊢ ∃ x ∈ V B ∈ W ∧ ψ ↔ B ∈ V ∧ ∃ x ∈ V B ∈ W ∧ ψ
15 10 14 bitr4i ⊢ B ∈ ⋃ ran ⁡ F ↔ ∃ x ∈ V B ∈ W ∧ ψ