Theorem preq2b

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

	Ref	Expression
Hypotheses	preq1b.a	|- ( ph -> A e. V )
	preq1b.b	|- ( ph -> B e. W )
Assertion	preq2b	|- ( ph -> ( { C , A } = { C , B } <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		preq1b.a	|- ( ph -> A e. V )
2		preq1b.b	|- ( ph -> B e. W )
3		prcom	|- { C , A } = { A , C }
4		prcom	|- { C , B } = { B , C }
5	3 4	eqeq12i	|- ( { C , A } = { C , B } <-> { A , C } = { B , C } )
6	1 2	preq1b	|- ( ph -> ( { A , C } = { B , C } <-> A = B ) )
7	5 6	bitrid	|- ( ph -> ( { C , A } = { C , B } <-> A = B ) )