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

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 ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ 𝑊 ∣ 𝜑 } )
rabfmpunirn.2 ⊢ 𝑊 ∈ V
rabfmpunirn.3 ⊢ ( 𝑦 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
Assertion rabfmpunirn ( 𝐵 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 rabfmpunirn.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ 𝑊 ∣ 𝜑 } )
2 rabfmpunirn.2 ⊢ 𝑊 ∈ V
3 rabfmpunirn.3 ⊢ ( 𝑦 = 𝐵 → ( 𝜑 ↔ 𝜓 ) )
4 df-rab ⊢ { 𝑦 ∈ 𝑊 ∣ 𝜑 } = { 𝑦 ∣ ( 𝑦 ∈ 𝑊 ∧ 𝜑 ) }
5 4 mpteq2i ⊢ ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∈ 𝑊 ∣ 𝜑 } ) = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∣ ( 𝑦 ∈ 𝑊 ∧ 𝜑 ) } )
6 1 5 eqtri ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ { 𝑦 ∣ ( 𝑦 ∈ 𝑊 ∧ 𝜑 ) } )
7 2 zfausab ⊢ { 𝑦 ∣ ( 𝑦 ∈ 𝑊 ∧ 𝜑 ) } ∈ V
8 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑊 ↔ 𝐵 ∈ 𝑊 ) )
9 8 3 anbi12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 ∈ 𝑊 ∧ 𝜑 ) ↔ ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) ) )
10 6 7 9 abfmpunirn ⊢ ( 𝐵 ∈ ∪ ran 𝐹 ↔ ( 𝐵 ∈ V ∧ ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) ) )
11 elex ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
12 11 adantr ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) → 𝐵 ∈ V )
13 12 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) → 𝐵 ∈ V )
14 13 pm4.71ri ⊢ ( ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) ↔ ( 𝐵 ∈ V ∧ ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) ) )
15 10 14 bitr4i ⊢ ( 𝐵 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) )