# Metamath Proof Explorer

## Theorem prtlem16

Description: Lemma for prtex , prter2 and prter3 . (Contributed by Rodolfo Medina, 14-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Hypothesis prtlem13.1
Assertion prtlem16

### Proof

Step Hyp Ref Expression
1 prtlem13.1
2 vex ${⊢}{z}\in \mathrm{V}$
3 2 eldm
4 1 prtlem13
5 4 exbii
6 elunii ${⊢}\left({z}\in {v}\wedge {v}\in {A}\right)\to {z}\in \bigcup {A}$
7 6 ancoms ${⊢}\left({v}\in {A}\wedge {z}\in {v}\right)\to {z}\in \bigcup {A}$
8 7 adantrr ${⊢}\left({v}\in {A}\wedge \left({z}\in {v}\wedge {w}\in {v}\right)\right)\to {z}\in \bigcup {A}$
9 8 rexlimiva ${⊢}\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}\in {v}\wedge {w}\in {v}\right)\to {z}\in \bigcup {A}$
10 9 exlimiv ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}\in {v}\wedge {w}\in {v}\right)\to {z}\in \bigcup {A}$
11 eluni2 ${⊢}{z}\in \bigcup {A}↔\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {v}$
12 elequ1 ${⊢}{w}={z}\to \left({w}\in {v}↔{z}\in {v}\right)$
13 12 anbi2d ${⊢}{w}={z}\to \left(\left({z}\in {v}\wedge {w}\in {v}\right)↔\left({z}\in {v}\wedge {z}\in {v}\right)\right)$
14 pm4.24 ${⊢}{z}\in {v}↔\left({z}\in {v}\wedge {z}\in {v}\right)$
15 13 14 syl6bbr ${⊢}{w}={z}\to \left(\left({z}\in {v}\wedge {w}\in {v}\right)↔{z}\in {v}\right)$
16 15 rexbidv ${⊢}{w}={z}\to \left(\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}\in {v}\wedge {w}\in {v}\right)↔\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {v}\right)$
17 2 16 spcev ${⊢}\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}{z}\in {v}\to \exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}\in {v}\wedge {w}\in {v}\right)$
18 11 17 sylbi ${⊢}{z}\in \bigcup {A}\to \exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}\in {v}\wedge {w}\in {v}\right)$
19 10 18 impbii ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\exists {v}\in {A}\phantom{\rule{.4em}{0ex}}\left({z}\in {v}\wedge {w}\in {v}\right)↔{z}\in \bigcup {A}$
20 3 5 19 3bitri
21 20 eqriv