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	⊢ Ⅎ 𝑥 𝐴
		elunif.2	⊢ Ⅎ 𝑥 𝐵
	Assertion	elunif	⊢ ( 𝐴 ∈ ∪ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		elunif.1	⊢ Ⅎ 𝑥 𝐴
2		elunif.2	⊢ Ⅎ 𝑥 𝐵
3		eluni	⊢ ( 𝐴 ∈ ∪ 𝐵 ↔ ∃ 𝑦 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) )
4		nfcv	⊢ Ⅎ 𝑥 𝑦
5	1 4	nfel	⊢ Ⅎ 𝑥 𝐴 ∈ 𝑦
6	4 2	nfel	⊢ Ⅎ 𝑥 𝑦 ∈ 𝐵
7	5 6	nfan	⊢ Ⅎ 𝑥 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 )
8		nfv	⊢ Ⅎ 𝑦 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 )
9		eleq2w	⊢ ( 𝑦 = 𝑥 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑥 ) )
10		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
11	9 10	anbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) ) )
12	7 8 11	cbvexv1	⊢ ( ∃ 𝑦 ( 𝐴 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵 ) ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) )
13	3 12	bitri	⊢ ( 𝐴 ∈ ∪ 𝐵 ↔ ∃ 𝑥 ( 𝐴 ∈ 𝑥 ∧ 𝑥 ∈ 𝐵 ) )