Theorem or2expropbilem2

Description: Lemma 2 for or2expropbi and ich2exprop . (Contributed by AV, 16-Jul-2023)

	Ref	Expression
Assertion	or2expropbilem2	$$⊢\exists a\exists b\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfv	$$⊢Ⅎx\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)$$
2		nfv	$$⊢Ⅎy\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)$$
3		nfv	$$⊢Ⅎa⟨A,B⟩=⟨x,y⟩$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}ay$$
5		nfsbc1v	$$⊢Ⅎa\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi$$
6	4 5	nfsbcw	$$⊢Ⅎa\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi$$
7	3 6	nfan	$$⊢Ⅎa\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
8		nfv	$$⊢Ⅎb⟨A,B⟩=⟨x,y⟩$$
9		nfsbc1v	$$⊢Ⅎb\underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi$$
10	8 9	nfan	$$⊢Ⅎb\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
11		opeq12	$$⊢\left(a=x\wedge b=y\right)\to ⟨a,b⟩=⟨x,y⟩$$
12	11	eqeq2d	$$⊢\left(a=x\wedge b=y\right)\to \left(⟨A,B⟩=⟨a,b⟩\leftrightarrow ⟨A,B⟩=⟨x,y⟩\right)$$
13		sbceq1a	$$⊢a=x\to \left(\phi \leftrightarrow \underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
14		sbceq1a	$$⊢b=y\to \left(\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
15	13 14	sylan9bb	$$⊢\left(a=x\wedge b=y\right)\to \left(\phi \leftrightarrow \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$
16	12 15	anbi12d	$$⊢\left(a=x\wedge b=y\right)\to \left(\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\leftrightarrow \left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)\right)$$
17	1 2 7 10 16	cbvex2v	$$⊢\exists a\exists b\left(⟨A,B⟩=⟨a,b⟩\wedge \phi \right)\leftrightarrow \exists x\exists y\left(⟨A,B⟩=⟨x,y⟩\wedge \underset{\dot{}}{[}y/b\underset{\dot{}}{]}\underset{\dot{}}{[}x/a\underset{\dot{}}{]}\phi \right)$$