Theorem sbcopeq1a

Description: Equality theorem for substitution of a class for an ordered pair (analogue of sbceq1a that avoids the existential quantifiers of copsexg ). (Contributed by NM, 19-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Assertion	sbcopeq1a	$$⊢A=⟨x,y⟩\to \left(\underset{\dot{}}{[}{1}^{st}\left(A\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(A\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2		vex	$$⊢y\in \mathrm{V}$$
3	1 2	op2ndd	$$⊢A=⟨x,y⟩\to 2^{nd}\left(A\right)=y$$
4	3	eqcomd	$$⊢A=⟨x,y⟩\to y=2^{nd}\left(A\right)$$
5		sbceq1a	$$⊢y=2^{nd}\left(A\right)\to \left(\phi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(A\right)/y\underset{\dot{}}{]}\phi \right)$$
6	4 5	syl	$$⊢A=⟨x,y⟩\to \left(\phi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(A\right)/y\underset{\dot{}}{]}\phi \right)$$
7	1 2	op1std	$$⊢A=⟨x,y⟩\to 1^{st}\left(A\right)=x$$
8	7	eqcomd	$$⊢A=⟨x,y⟩\to x=1^{st}\left(A\right)$$
9		sbceq1a	$$⊢x=1^{st}\left(A\right)\to \left(\underset{\dot{}}{[}{2}^{nd}\left(A\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(A\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(A\right)/y\underset{\dot{}}{]}\phi \right)$$
10	8 9	syl	$$⊢A=⟨x,y⟩\to \left(\underset{\dot{}}{[}{2}^{nd}\left(A\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(A\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(A\right)/y\underset{\dot{}}{]}\phi \right)$$
11	6 10	bitr2d	$$⊢A=⟨x,y⟩\to \left(\underset{\dot{}}{[}{1}^{st}\left(A\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(A\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$