Theorem dfdisj2

Description: Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017)

	Ref	Expression
Assertion	dfdisj2	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall y{\exists }^{*}x\left(x\in A\wedge y\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-disj	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall y{\exists }^{*}x\in Ay\in B$$
2		df-rmo	$$⊢{\exists }^{*}x\in Ay\in B\leftrightarrow {\exists }^{*}x\left(x\in A\wedge y\in B\right)$$
3	2	albii	$$⊢\forall y{\exists }^{*}x\in Ay\in B\leftrightarrow \forall y{\exists }^{*}x\left(x\in A\wedge y\in B\right)$$
4	1 3	bitri	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall y{\exists }^{*}x\left(x\in A\wedge y\in B\right)$$