Theorem opeq2

Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998) (Revised by Mario Carneiro, 26-Apr-2015)

	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	1	anbi2d	$$⊢A=B\to \left(\left(C\in \mathrm{V}\wedge A\in \mathrm{V}\right)\leftrightarrow \left(C\in \mathrm{V}\wedge B\in \mathrm{V}\right)\right)$$
3		preq2	$$⊢A=B\to \left\{C,A\right\}=\left\{C,B\right\}$$
4	3	preq2d	$$⊢A=B\to \left\{\left\{C\right\},\left\{C,A\right\}\right\}=\left\{\left\{C\right\},\left\{C,B\right\}\right\}$$
5	2 4	ifbieq1d	$$⊢A=B\to if\left(\left(C\in \mathrm{V}\wedge A\in \mathrm{V}\right),\left\{\left\{C\right\},\left\{C,A\right\}\right\},\varnothing \right)=if\left(\left(C\in \mathrm{V}\wedge B\in \mathrm{V}\right),\left\{\left\{C\right\},\left\{C,B\right\}\right\},\varnothing \right)$$
6		dfopif	$$⊢⟨C,A⟩=if\left(\left(C\in \mathrm{V}\wedge A\in \mathrm{V}\right),\left\{\left\{C\right\},\left\{C,A\right\}\right\},\varnothing \right)$$
7		dfopif	$$⊢⟨C,B⟩=if\left(\left(C\in \mathrm{V}\wedge B\in \mathrm{V}\right),\left\{\left\{C\right\},\left\{C,B\right\}\right\},\varnothing \right)$$
8	5 6 7	3eqtr4g	$$⊢A=B\to ⟨C,A⟩=⟨C,B⟩$$