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

Metamath Proof Explorer

Theorem difjust

Description: Soundness justification theorem for df-dif . (Contributed by Rodolfo Medina, 27-Apr-2010) (Proof shortened by Andrew Salmon, 9-Jul-2011)

		Ref	Expression
	Assertion	difjust	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) }

Proof

Step	Hyp	Ref	Expression
1		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 ) )
2		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
3	2	notbid	⊢ ( 𝑥 = 𝑧 → ( ¬ 𝑥 ∈ 𝐵 ↔ ¬ 𝑧 ∈ 𝐵 ) )
4	1 3	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) ↔ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝐵 ) ) )
5	4	cbvabv	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) } = { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝐵 ) }
6		eleq1w	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) )
7		eleq1w	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
8	7	notbid	⊢ ( 𝑧 = 𝑦 → ( ¬ 𝑧 ∈ 𝐵 ↔ ¬ 𝑦 ∈ 𝐵 ) )
9	6 8	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝐵 ) ↔ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) ) )
10	9	cbvabv	⊢ { 𝑧 ∣ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝐵 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) }
11	5 10	eqtri	⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝐵 ) }