Theorem dfeldisj4

Description: Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021)

	Ref	Expression
Assertion	dfeldisj4	$$⊢ElDisjA\leftrightarrow \forall x{\exists }^{*}u\in Ax\in u$$

Proof

Step	Hyp	Ref	Expression
1		df-eldisj	$$⊢ElDisjA\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
2		relres	$$⊢\mathrm{Rel}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
3		dfdisjALTV4	$$⊢Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\leftrightarrow \left(\forall x{\exists }^{*}uu\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)x\wedge \mathrm{Rel}\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\right)$$
4	2 3	mpbiran2	$$⊢Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\leftrightarrow \forall x{\exists }^{*}uu\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)x$$
5		brcnvepres	$$⊢\left(u\in \mathrm{V}\wedge x\in \mathrm{V}\right)\to \left(u\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)x\leftrightarrow \left(u\in A\wedge x\in u\right)\right)$$
6	5	el2v	$$⊢u\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)x\leftrightarrow \left(u\in A\wedge x\in u\right)$$
7	6	mobii	$$⊢{\exists }^{*}uu\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)x\leftrightarrow {\exists }^{*}u\left(u\in A\wedge x\in u\right)$$
8		df-rmo	$$⊢{\exists }^{*}u\in Ax\in u\leftrightarrow {\exists }^{*}u\left(u\in A\wedge x\in u\right)$$
9	7 8	bitr4i	$$⊢{\exists }^{*}uu\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)x\leftrightarrow {\exists }^{*}u\in Ax\in u$$
10	9	albii	$$⊢\forall x{\exists }^{*}uu\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)x\leftrightarrow \forall x{\exists }^{*}u\in Ax\in u$$
11	1 4 10	3bitri	$$⊢ElDisjA\leftrightarrow \forall x{\exists }^{*}u\in Ax\in u$$