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	|- F/_ x A
	elunif.2	|- F/_ x B
Assertion	elunif	|- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )

Proof

Step	Hyp	Ref	Expression
1		elunif.1	|- F/_ x A
2		elunif.2	|- F/_ x B
3		eluni	|- ( A e. U. B <-> E. y ( A e. y /\ y e. B ) )
4		nfcv	|- F/_ x y
5	1 4	nfel	|- F/ x A e. y
6	4 2	nfel	|- F/ x y e. B
7	5 6	nfan	|- F/ x ( A e. y /\ y e. B )
8		nfv	|- F/ y ( A e. x /\ x e. B )
9		eleq2w	|- ( y = x -> ( A e. y <-> A e. x ) )
10		eleq1w	|- ( y = x -> ( y e. B <-> x e. B ) )
11	9 10	anbi12d	|- ( y = x -> ( ( A e. y /\ y e. B ) <-> ( A e. x /\ x e. B ) ) )
12	7 8 11	cbvexv1	|- ( E. y ( A e. y /\ y e. B ) <-> E. x ( A e. x /\ x e. B ) )
13	3 12	bitri	|- ( A e. U. B <-> E. x ( A e. x /\ x e. B ) )