Metamath Proof Explorer

Theorem eldisjn0elb

Description: Two forms of disjoint elements when the empty set is not an element of the class. (Contributed by Peter Mazsa, 31-Dec-2024)

		Ref	Expression
	Assertion	eldisjn0elb	\|- ( ( ElDisj A /\ -. (/) e. A ) <-> ( Disj ( `' _E \|` A ) /\ ( dom ( `' _E \|` A ) /. ( `' _E \|` A ) ) = A ) )

Step	Hyp	Ref	Expression
1		df-eldisj	\|- ( ElDisj A <-> Disj ( `' _E \|` A ) )
2		n0el3	\|- ( -. (/) e. A <-> ( dom ( `' _E \|` A ) /. ( `' _E \|` A ) ) = A )
3	1 2	anbi12i	\|- ( ( ElDisj A /\ -. (/) e. A ) <-> ( Disj ( `' _E \|` A ) /\ ( dom ( `' _E \|` A ) /. ( `' _E \|` A ) ) = A ) )

Step

Hyp

Ref

Expression

 |-  ( ElDisj A <-> Disj ( `' _E |` A ) )

 |-  ( -. (/) e. A <-> ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A )

1 2

 |-  ( ( ElDisj A /\ -. (/) e. A ) <-> ( Disj ( `' _E |` A ) /\ ( dom ( `' _E |` A ) /. ( `' _E |` A ) ) = A ) )