This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )