Theorem sbcralt

Description: Interchange class substitution and restricted quantifier. (Contributed by NM, 1-Mar-2008) (Revised by David Abernethy, 22-Feb-2010)

	Ref	Expression
Assertion	sbcralt	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}yA\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in B\phi \leftrightarrow \forall y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbccow	$$⊢\underset{\dot{}}{[}A/z\underset{\dot{}}{]}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\forall y\in B\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in B\phi$$
2		simpl	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}yA\right)\to A\in V$$
3		sbsbc	$$⊢\left[z/x\right]\forall y\in B\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\forall y\in B\phi$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
5		nfs1v	$$⊢Ⅎx\left[z/x\right]\phi$$
6	4 5	nfralw	$$⊢Ⅎx\forall y\in B\left[z/x\right]\phi$$
7		sbequ12	$$⊢x=z\to \left(\phi \leftrightarrow \left[z/x\right]\phi \right)$$
8	7	ralbidv	$$⊢x=z\to \left(\forall y\in B\phi \leftrightarrow \forall y\in B\left[z/x\right]\phi \right)$$
9	6 8	sbiev	$$⊢\left[z/x\right]\forall y\in B\phi \leftrightarrow \forall y\in B\left[z/x\right]\phi$$
10	3 9	bitr3i	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\forall y\in B\phi \leftrightarrow \forall y\in B\left[z/x\right]\phi$$
11		nfnfc1	$$⊢Ⅎy\underset{\_}{Ⅎ}yA$$
12		nfcvd	$$⊢\underset{\_}{Ⅎ}yA\to \underset{\_}{Ⅎ}yz$$
13		id	$$⊢\underset{\_}{Ⅎ}yA\to \underset{\_}{Ⅎ}yA$$
14	12 13	nfeqd	$$⊢\underset{\_}{Ⅎ}yA\to Ⅎyz=A$$
15	11 14	nfan1	$$⊢Ⅎy\left(\underset{\_}{Ⅎ}yA\wedge z=A\right)$$
16		dfsbcq2	$$⊢z=A\to \left(\left[z/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
17	16	adantl	$$⊢\left(\underset{\_}{Ⅎ}yA\wedge z=A\right)\to \left(\left[z/x\right]\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
18	15 17	ralbid	$$⊢\left(\underset{\_}{Ⅎ}yA\wedge z=A\right)\to \left(\forall y\in B\left[z/x\right]\phi \leftrightarrow \forall y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
19	18	adantll	$$⊢\left(\left(A\in V\wedge \underset{\_}{Ⅎ}yA\right)\wedge z=A\right)\to \left(\forall y\in B\left[z/x\right]\phi \leftrightarrow \forall y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
20	10 19	bitrid	$$⊢\left(\left(A\in V\wedge \underset{\_}{Ⅎ}yA\right)\wedge z=A\right)\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\forall y\in B\phi \leftrightarrow \forall y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
21	2 20	sbcied	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}yA\right)\to \left(\underset{\dot{}}{[}A/z\underset{\dot{}}{]}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\forall y\in B\phi \leftrightarrow \forall y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
22	1 21	bitr3id	$$⊢\left(A\in V\wedge \underset{\_}{Ⅎ}yA\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\forall y\in B\phi \leftrightarrow \forall y\in B\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$