Theorem elunif

Description: A version of eluni using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	elunif.1	$$⊢\underset{\_}{Ⅎ}xA$$
	elunif.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	elunif	$$⊢A\in \bigcup B\leftrightarrow \exists x\left(A\in x\wedge x\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elunif.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		elunif.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		eluni	$$⊢A\in \bigcup B\leftrightarrow \exists y\left(A\in y\wedge y\in B\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
5	1 4	nfel	$$⊢ℲxA\in y$$
6	4 2	nfel	$$⊢Ⅎxy\in B$$
7	5 6	nfan	$$⊢Ⅎx\left(A\in y\wedge y\in B\right)$$
8		nfv	$$⊢Ⅎy\left(A\in x\wedge x\in B\right)$$
9		eleq2w	$$⊢y=x\to \left(A\in y\leftrightarrow A\in x\right)$$
10		eleq1w	$$⊢y=x\to \left(y\in B\leftrightarrow x\in B\right)$$
11	9 10	anbi12d	$$⊢y=x\to \left(\left(A\in y\wedge y\in B\right)\leftrightarrow \left(A\in x\wedge x\in B\right)\right)$$
12	7 8 11	cbvexv1	$$⊢\exists y\left(A\in y\wedge y\in B\right)\leftrightarrow \exists x\left(A\in x\wedge x\in B\right)$$
13	3 12	bitri	$$⊢A\in \bigcup B\leftrightarrow \exists x\left(A\in x\wedge x\in B\right)$$