This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 \in S \land B \in S) \to dom ⟨“ A B ”⟩ = \{0, 1\}$

Proof

Step	Hyp	Ref	Expression
1		s2prop	$⊢ (A \in S \land B \in S) \to ⟨“ A B ”⟩ = \{⟨0, A⟩, ⟨1, B⟩\}$
2	1	dmeqd	$⊢ (A \in S \land B \in S) \to dom ⟨“ A B ”⟩ = dom \{⟨0, A⟩, ⟨1, B⟩\}$
3		dmpropg	$⊢ (A \in S \land B \in S) \to dom \{⟨0, A⟩, ⟨1, B⟩\} = \{0, 1\}$
4	2 3	eqtrd	$⊢ (A \in S \land B \in S) \to dom ⟨“ A B ”⟩ = \{0, 1\}$