Theorem dfeldisj4

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

	Ref	Expression
Assertion	dfeldisj4	|- ( ElDisj A <-> A. x E* u e. A x e. u )

Proof

Step	Hyp	Ref	Expression
1		df-eldisj	|- ( ElDisj A <-> Disj ( `' _E |` A ) )
2		relres	|- Rel ( `' _E |` A )
3		dfdisjALTV4	|- ( Disj ( `' _E |` A ) <-> ( A. x E* u u ( `' _E |` A ) x /\ Rel ( `' _E |` A ) ) )
4	2 3	mpbiran2	|- ( Disj ( `' _E |` A ) <-> A. x E* u u ( `' _E |` A ) x )
5		brcnvepres	|- ( ( u e. _V /\ x e. _V ) -> ( u ( `' _E |` A ) x <-> ( u e. A /\ x e. u ) ) )
6	5	el2v	|- ( u ( `' _E |` A ) x <-> ( u e. A /\ x e. u ) )
7	6	mobii	|- ( E* u u ( `' _E |` A ) x <-> E* u ( u e. A /\ x e. u ) )
8		df-rmo	|- ( E* u e. A x e. u <-> E* u ( u e. A /\ x e. u ) )
9	7 8	bitr4i	|- ( E* u u ( `' _E |` A ) x <-> E* u e. A x e. u )
10	9	albii	|- ( A. x E* u u ( `' _E |` A ) x <-> A. x E* u e. A x e. u )
11	1 4 10	3bitri	|- ( ElDisj A <-> A. x E* u e. A x e. u )