Theorem untuni

Description: The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011)

	Ref	Expression
Assertion	untuni	$$⊢\forall x\in \bigcup A\neg x\in x\leftrightarrow \forall y\in A\forall x\in y\neg x\in x$$

Proof

Step	Hyp	Ref	Expression
1		r19.23v	$$⊢\forall y\in A\left(x\in y\to \neg x\in x\right)\leftrightarrow \left(\exists y\in Ax\in y\to \neg x\in x\right)$$
2	1	albii	$$⊢\forall x\forall y\in A\left(x\in y\to \neg x\in x\right)\leftrightarrow \forall x\left(\exists y\in Ax\in y\to \neg x\in x\right)$$
3		ralcom4	$$⊢\forall y\in A\forall x\left(x\in y\to \neg x\in x\right)\leftrightarrow \forall x\forall y\in A\left(x\in y\to \neg x\in x\right)$$
4		eluni2	$$⊢x\in \bigcup A\leftrightarrow \exists y\in Ax\in y$$
5	4	imbi1i	$$⊢\left(x\in \bigcup A\to \neg x\in x\right)\leftrightarrow \left(\exists y\in Ax\in y\to \neg x\in x\right)$$
6	5	albii	$$⊢\forall x\left(x\in \bigcup A\to \neg x\in x\right)\leftrightarrow \forall x\left(\exists y\in Ax\in y\to \neg x\in x\right)$$
7	2 3 6	3bitr4ri	$$⊢\forall x\left(x\in \bigcup A\to \neg x\in x\right)\leftrightarrow \forall y\in A\forall x\left(x\in y\to \neg x\in x\right)$$
8		df-ral	$$⊢\forall x\in \bigcup A\neg x\in x\leftrightarrow \forall x\left(x\in \bigcup A\to \neg x\in x\right)$$
9		df-ral	$$⊢\forall x\in y\neg x\in x\leftrightarrow \forall x\left(x\in y\to \neg x\in x\right)$$
10	9	ralbii	$$⊢\forall y\in A\forall x\in y\neg x\in x\leftrightarrow \forall y\in A\forall x\left(x\in y\to \neg x\in x\right)$$
11	7 8 10	3bitr4i	$$⊢\forall x\in \bigcup A\neg x\in x\leftrightarrow \forall y\in A\forall x\in y\neg x\in x$$