difsnen

Description: All decrements of a set are equinumerous. (Contributed by Stefan O'Rear, 19-Feb-2015)

		Ref	Expression
	Assertion	difsnen	$⊢ (X \in V \land A \in X \land B \in X) \to (X ∖ \{A\}) \approx (X ∖ \{B\})$

Proof

Step	Hyp	Ref	Expression
1		difexg	$⊢ X \in V \to X ∖ \{A\} \in V$
2		enrefg	$⊢ X ∖ \{A\} \in V \to (X ∖ \{A\}) \approx (X ∖ \{A\})$
3	1 2	syl	$⊢ X \in V \to (X ∖ \{A\}) \approx (X ∖ \{A\})$
4	3	3ad2ant1	$⊢ (X \in V \land A \in X \land B \in X) \to (X ∖ \{A\}) \approx (X ∖ \{A\})$
5		sneq	$⊢ A = B \to \{A\} = \{B\}$
6	5	difeq2d	$⊢ A = B \to X ∖ \{A\} = X ∖ \{B\}$
7	6	breq2d	$⊢ A = B \to ((X ∖ \{A\}) \approx (X ∖ \{A\}) \leftrightarrow (X ∖ \{A\}) \approx (X ∖ \{B\}))$
8	4 7	syl5ibcom	$⊢ (X \in V \land A \in X \land B \in X) \to (A = B \to (X ∖ \{A\}) \approx (X ∖ \{B\}))$
9	8	imp	$⊢ ((X \in V \land A \in X \land B \in X) \land A = B) \to (X ∖ \{A\}) \approx (X ∖ \{B\})$
10		simpl1	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to X \in V$
11		difexg	$⊢ X ∖ \{A\} \in V \to (X ∖ \{A\}) ∖ \{B\} \in V$
12		enrefg	$⊢ (X ∖ \{A\}) ∖ \{B\} \in V \to ((X ∖ \{A\}) ∖ \{B\}) \approx ((X ∖ \{A\}) ∖ \{B\})$
13	10 1 11 12	4syl	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{A\}) ∖ \{B\}) \approx ((X ∖ \{A\}) ∖ \{B\})$
14		dif32	$⊢ (X ∖ \{A\}) ∖ \{B\} = (X ∖ \{B\}) ∖ \{A\}$
15	13 14	breqtrdi	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{A\}) ∖ \{B\}) \approx ((X ∖ \{B\}) ∖ \{A\})$
16		simpl3	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to B \in X$
17		simpl2	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to A \in X$
18		en2sn	$⊢ (B \in X \land A \in X) \to \{B\} \approx \{A\}$
19	16 17 18	syl2anc	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to \{B\} \approx \{A\}$
20		disjdifr	$⊢ ((X ∖ \{A\}) ∖ \{B\}) \cap \{B\} = \emptyset$
21	20	a1i	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{A\}) ∖ \{B\}) \cap \{B\} = \emptyset$
22		disjdifr	$⊢ ((X ∖ \{B\}) ∖ \{A\}) \cap \{A\} = \emptyset$
23	22	a1i	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{B\}) ∖ \{A\}) \cap \{A\} = \emptyset$
24		unen	$⊢ ((((X ∖ \{A\}) ∖ \{B\}) \approx ((X ∖ \{B\}) ∖ \{A\}) \land \{B\} \approx \{A\}) \land (((X ∖ \{A\}) ∖ \{B\}) \cap \{B\} = \emptyset \land ((X ∖ \{B\}) ∖ \{A\}) \cap \{A\} = \emptyset)) \to (((X ∖ \{A\}) ∖ \{B\}) \cup \{B\}) \approx (((X ∖ \{B\}) ∖ \{A\}) \cup \{A\})$
25	15 19 21 23 24	syl22anc	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to (((X ∖ \{A\}) ∖ \{B\}) \cup \{B\}) \approx (((X ∖ \{B\}) ∖ \{A\}) \cup \{A\})$
26		simpr	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to A \neq B$
27	26	necomd	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to B \neq A$
28		eldifsn	$⊢ B \in (X ∖ \{A\}) \leftrightarrow (B \in X \land B \neq A)$
29	16 27 28	sylanbrc	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to B \in (X ∖ \{A\})$
30		difsnid	$⊢ B \in (X ∖ \{A\}) \to ((X ∖ \{A\}) ∖ \{B\}) \cup \{B\} = X ∖ \{A\}$
31	29 30	syl	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{A\}) ∖ \{B\}) \cup \{B\} = X ∖ \{A\}$
32		eldifsn	$⊢ A \in (X ∖ \{B\}) \leftrightarrow (A \in X \land A \neq B)$
33	17 26 32	sylanbrc	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to A \in (X ∖ \{B\})$
34		difsnid	$⊢ A \in (X ∖ \{B\}) \to ((X ∖ \{B\}) ∖ \{A\}) \cup \{A\} = X ∖ \{B\}$
35	33 34	syl	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to ((X ∖ \{B\}) ∖ \{A\}) \cup \{A\} = X ∖ \{B\}$
36	25 31 35	3brtr3d	$⊢ ((X \in V \land A \in X \land B \in X) \land A \neq B) \to (X ∖ \{A\}) \approx (X ∖ \{B\})$
37	9 36	pm2.61dane	$⊢ (X \in V \land A \in X \land B \in X) \to (X ∖ \{A\}) \approx (X ∖ \{B\})$

Metamath Proof Explorer

Theorem difsnen

Proof