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 𝐹 ↔ ∃ 𝑥 ∈ 𝑉 ( 𝐵 ∈ 𝑊 ∧ 𝜓 ) )