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		sepab	⊢ ( 𝑊 ∈ V → { 𝑦 ∣ ( 𝑦 ∈ 𝑊 ∧ 𝜑 ) } ∈ V )
8	2 7	ax-mp	⊢ { 𝑦 ∣ ( 𝑦 ∈ 𝑊 ∧ 𝜑 ) } ∈ V
9		eleq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑊 ↔ 𝐵 ∈ 𝑊 ) )
10	9 3	anbi12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝑦 ∈ 𝑊 ∧ 𝜑 ) ↔ ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) ) )
11	6 8 10	abfmpunirn	⊢ ( 𝐵 ∈ ∪ ran 𝐹 ↔ ( 𝐵 ∈ V ∧ ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) ) )
12		elex	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ V )
13	12	adantr	⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) → 𝐵 ∈ V )
14	13	rexlimivw	⊢ ( ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) → 𝐵 ∈ V )
15	14	pm4.71ri	⊢ ( ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) ↔ ( 𝐵 ∈ V ∧ ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) ) )
16	11 15	bitr4i	⊢ ( 𝐵 ∈ ∪ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) )