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

Metamath Proof Explorer

Theorem qdassr

Description: Two ways to write an unordered quadruple. (Contributed by Mario Carneiro, 5-Jan-2016)

		Ref	Expression
	Assertion	qdassr	$⊢ \{A, B\} \cup \{C, D\} = \{A\} \cup \{B, C, D\}$

Step	Hyp	Ref	Expression
1		unass	$⊢ (\{A\} \cup \{B\}) \cup \{C, D\} = \{A\} \cup (\{B\} \cup \{C, D\})$
2		df-pr	$⊢ \{A, B\} = \{A\} \cup \{B\}$
3	2	uneq1i	$⊢ \{A, B\} \cup \{C, D\} = (\{A\} \cup \{B\}) \cup \{C, D\}$
4		tpass	$⊢ \{B, C, D\} = \{B\} \cup \{C, D\}$
5	4	uneq2i	$⊢ \{A\} \cup \{B, C, D\} = \{A\} \cup (\{B\} \cup \{C, D\})$
6	1 3 5	3eqtr4i	$⊢ \{A, B\} \cup \{C, D\} = \{A\} \cup \{B, C, D\}$