Theorem opeq2

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015) Avoid ax-10 , ax-11 , ax-12 . (Revised by Gino Giotto, 26-May-2024)

	Ref	Expression
Assertion	opeq2	$$⊢A=B\to ⟨C,A⟩=⟨C,B⟩$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢A=B\to \left(A\in \mathrm{V}\leftrightarrow B\in \mathrm{V}\right)$$
2		preq2	$$⊢A=B\to \left\{C,A\right\}=\left\{C,B\right\}$$
3	2	preq2d	$$⊢A=B\to \left\{\left\{C\right\},\left\{C,A\right\}\right\}=\left\{\left\{C\right\},\left\{C,B\right\}\right\}$$
4	3	eleq2d	$$⊢A=B\to \left(x\in \left\{\left\{C\right\},\left\{C,A\right\}\right\}\leftrightarrow x\in \left\{\left\{C\right\},\left\{C,B\right\}\right\}\right)$$
5	1 4	3anbi23d	$$⊢A=B\to \left(\left(C\in \mathrm{V}\wedge A\in \mathrm{V}\wedge x\in \left\{\left\{C\right\},\left\{C,A\right\}\right\}\right)\leftrightarrow \left(C\in \mathrm{V}\wedge B\in \mathrm{V}\wedge x\in \left\{\left\{C\right\},\left\{C,B\right\}\right\}\right)\right)$$
6	5	abbidv	$$⊢A=B\to \left\{x|\left(C\in \mathrm{V}\wedge A\in \mathrm{V}\wedge x\in \left\{\left\{C\right\},\left\{C,A\right\}\right\}\right)\right\}=\left\{x|\left(C\in \mathrm{V}\wedge B\in \mathrm{V}\wedge x\in \left\{\left\{C\right\},\left\{C,B\right\}\right\}\right)\right\}$$
7		df-op	$$⊢⟨C,A⟩=\left\{x|\left(C\in \mathrm{V}\wedge A\in \mathrm{V}\wedge x\in \left\{\left\{C\right\},\left\{C,A\right\}\right\}\right)\right\}$$
8		df-op	$$⊢⟨C,B⟩=\left\{x|\left(C\in \mathrm{V}\wedge B\in \mathrm{V}\wedge x\in \left\{\left\{C\right\},\left\{C,B\right\}\right\}\right)\right\}$$
9	6 7 8	3eqtr4g	$$⊢A=B\to ⟨C,A⟩=⟨C,B⟩$$