Theorem s2dmALT

Description: Alternate version of s2dm , having a shorter proof, but requiring that A and B are sets. (Contributed by AV, 9-Jan-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	s2dmALT	|- ( ( A e. S /\ B e. S ) -> dom <" A B "> = { 0 , 1 } )

Proof

Step	Hyp	Ref	Expression
1		s2prop	|- ( ( A e. S /\ B e. S ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
2	1	dmeqd	|- ( ( A e. S /\ B e. S ) -> dom <" A B "> = dom { <. 0 , A >. , <. 1 , B >. } )
3		dmpropg	|- ( ( A e. S /\ B e. S ) -> dom { <. 0 , A >. , <. 1 , B >. } = { 0 , 1 } )
4	2 3	eqtrd	|- ( ( A e. S /\ B e. S ) -> dom <" A B "> = { 0 , 1 } )