Theorem preq1b

Description: Biconditional equality lemma for unordered pairs, deduction form. Two unordered pairs have the same second element iff the first elements are equal. (Contributed by AV, 18-Dec-2020)

	Ref	Expression
Hypotheses	preq1b.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	preq1b.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion	preq1b	⊢ ( 𝜑 → ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		preq1b.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		preq1b.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3		prid1g	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐶 } )
4	1 3	syl	⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 , 𝐶 } )
5		eleq2	⊢ ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } → ( 𝐴 ∈ { 𝐴 , 𝐶 } ↔ 𝐴 ∈ { 𝐵 , 𝐶 } ) )
6	4 5	syl5ibcom	⊢ ( 𝜑 → ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } → 𝐴 ∈ { 𝐵 , 𝐶 } ) )
7		elprg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
8	1 7	syl	⊢ ( 𝜑 → ( 𝐴 ∈ { 𝐵 , 𝐶 } ↔ ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
9	6 8	sylibd	⊢ ( 𝜑 → ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } → ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) ) )
10	9	imp	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } ) → ( 𝐴 = 𝐵 ∨ 𝐴 = 𝐶 ) )
11		prid1g	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐵 , 𝐶 } )
12	2 11	syl	⊢ ( 𝜑 → 𝐵 ∈ { 𝐵 , 𝐶 } )
13		eleq2	⊢ ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } → ( 𝐵 ∈ { 𝐴 , 𝐶 } ↔ 𝐵 ∈ { 𝐵 , 𝐶 } ) )
14	12 13	syl5ibrcom	⊢ ( 𝜑 → ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } → 𝐵 ∈ { 𝐴 , 𝐶 } ) )
15		elprg	⊢ ( 𝐵 ∈ 𝑊 → ( 𝐵 ∈ { 𝐴 , 𝐶 } ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) )
16	2 15	syl	⊢ ( 𝜑 → ( 𝐵 ∈ { 𝐴 , 𝐶 } ↔ ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) )
17	14 16	sylibd	⊢ ( 𝜑 → ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } → ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) ) )
18	17	imp	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } ) → ( 𝐵 = 𝐴 ∨ 𝐵 = 𝐶 ) )
19		eqcom	⊢ ( 𝐴 = 𝐵 ↔ 𝐵 = 𝐴 )
20		eqeq2	⊢ ( 𝐴 = 𝐶 → ( 𝐵 = 𝐴 ↔ 𝐵 = 𝐶 ) )
21	10 18 19 20	oplem1	⊢ ( ( 𝜑 ∧ { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } ) → 𝐴 = 𝐵 )
22	21	ex	⊢ ( 𝜑 → ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } → 𝐴 = 𝐵 ) )
23		preq1	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } )
24	22 23	impbid1	⊢ ( 𝜑 → ( { 𝐴 , 𝐶 } = { 𝐵 , 𝐶 } ↔ 𝐴 = 𝐵 ) )