Theorem elmptrab

Description: Membership in a one-parameter class of sets. (Contributed by Stefan O'Rear, 28-Jul-2015)

	Ref	Expression
Hypotheses	elmptrab.f	$$⊢F=\left(x\in D⟼\left\{y\in B|\phi \right\}\right)$$
	elmptrab.s1	$$⊢\left(x=X\wedge y=Y\right)\to \left(\phi \leftrightarrow \psi \right)$$
	elmptrab.s2	$$⊢x=X\to B=C$$
	elmptrab.ex	$$⊢x\in D\to B\in V$$
Assertion	elmptrab	$$⊢Y\in F\left(X\right)\leftrightarrow \left(X\in D\wedge Y\in C\wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		elmptrab.f	$$⊢F=\left(x\in D⟼\left\{y\in B|\phi \right\}\right)$$
2		elmptrab.s1	$$⊢\left(x=X\wedge y=Y\right)\to \left(\phi \leftrightarrow \psi \right)$$
3		elmptrab.s2	$$⊢x=X\to B=C$$
4		elmptrab.ex	$$⊢x\in D\to B\in V$$
5	1	mptrcl	$$⊢Y\in F\left(X\right)\to X\in D$$
6		simp1	$$⊢\left(X\in D\wedge Y\in C\wedge \psi \right)\to X\in D$$
7		csbeq1	$$⊢z=X\to ⦋z/x⦌B=⦋X/x⦌B$$
8		dfsbcq	$$⊢z=X\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right)$$
9	7 8	rabeqbidv	$$⊢z=X\to \left\{w\in ⦋z/x⦌B|\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}=\left\{w\in ⦋X/x⦌B|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}z\left\{y\in B|\phi \right\}$$
11		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi$$
12		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌B$$
13	11 12	nfrabw	$$⊢\underset{\_}{Ⅎ}x\left\{w\in ⦋z/x⦌B|\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}$$
14		csbeq1a	$$⊢x=z\to B=⦋z/x⦌B$$
15		sbceq1a	$$⊢x=z\to \left(\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
16	14 15	rabeqbidv	$$⊢x=z\to \left\{y\in B|\phi \right\}=\left\{y\in ⦋z/x⦌B|\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right\}$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}w⦋z/x⦌B$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}y⦋z/x⦌B$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}yz$$
20		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi$$
21	19 20	nfsbcw	$$⊢Ⅎy\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi$$
22		nfv	$$⊢Ⅎw\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
23		sbceq1a	$$⊢y=w\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
24	23	equcoms	$$⊢w=y\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
25		sbccom	$$⊢\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}w/y\underset{\dot{}}{]}\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi$$
26	24 25	syl6rbbr	$$⊢w=y\to \left(\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right)$$
27	17 18 21 22 26	cbvrabw	$$⊢\left\{w\in ⦋z/x⦌B|\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}=\left\{y\in ⦋z/x⦌B|\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\phi \right\}$$
28	16 27	eqtr4di	$$⊢x=z\to \left\{y\in B|\phi \right\}=\left\{w\in ⦋z/x⦌B|\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}$$
29	10 13 28	cbvmpt	$$⊢\left(x\in D⟼\left\{y\in B|\phi \right\}\right)=\left(z\in D⟼\left\{w\in ⦋z/x⦌B|\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}\right)$$
30	1 29	eqtri	$$⊢F=\left(z\in D⟼\left\{w\in ⦋z/x⦌B|\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}\right)$$
31		nfv	$$⊢Ⅎxz\in D$$
32	12	nfel1	$$⊢Ⅎx⦋z/x⦌B\in V$$
33	31 32	nfim	$$⊢Ⅎx\left(z\in D\to ⦋z/x⦌B\in V\right)$$
34		eleq1w	$$⊢x=z\to \left(x\in D\leftrightarrow z\in D\right)$$
35	14	eleq1d	$$⊢x=z\to \left(B\in V\leftrightarrow ⦋z/x⦌B\in V\right)$$
36	34 35	imbi12d	$$⊢x=z\to \left(\left(x\in D\to B\in V\right)\leftrightarrow \left(z\in D\to ⦋z/x⦌B\in V\right)\right)$$
37	33 36 4	chvarfv	$$⊢z\in D\to ⦋z/x⦌B\in V$$
38		rabexg	$$⊢⦋z/x⦌B\in V\to \left\{w\in ⦋z/x⦌B|\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}$$
39	37 38	syl	$$⊢z\in D\to \left\{w\in ⦋z/x⦌B|\underset{\dot{}}{[}z/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}\in \mathrm{V}$$
40	9 30 39	fvmpt3	$$⊢X\in D\to F\left(X\right)=\left\{w\in ⦋X/x⦌B|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}$$
41	40	eleq2d	$$⊢X\in D\to \left(Y\in F\left(X\right)\leftrightarrow Y\in \left\{w\in ⦋X/x⦌B|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}\right)$$
42		dfsbcq	$$⊢w=Y\to \left(\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right)$$
43	42	sbcbidv	$$⊢w=Y\to \left(\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right)$$
44	43	elrab	$$⊢Y\in \left\{w\in ⦋X/x⦌B|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}\leftrightarrow \left(Y\in ⦋X/x⦌B\wedge \underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right)$$
45	44	a1i	$$⊢X\in D\to \left(Y\in \left\{w\in ⦋X/x⦌B|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}\leftrightarrow \left(Y\in ⦋X/x⦌B\wedge \underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right)\right)$$
46		nfcvd	$$⊢X\in D\to \underset{\_}{Ⅎ}xC$$
47	46 3	csbiegf	$$⊢X\in D\to ⦋X/x⦌B=C$$
48	47	eleq2d	$$⊢X\in D\to \left(Y\in ⦋X/x⦌B\leftrightarrow Y\in C\right)$$
49	48	anbi1d	$$⊢X\in D\to \left(\left(Y\in ⦋X/x⦌B\wedge \underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(Y\in C\wedge \underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right)\right)$$
50		nfv	$$⊢Ⅎx\psi$$
51		nfv	$$⊢Ⅎy\psi$$
52		nfv	$$⊢ℲxY\in C$$
53	50 51 52 2	sbc2iegf	$$⊢\left(X\in D\wedge Y\in C\right)\to \left(\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
54	53	pm5.32da	$$⊢X\in D\to \left(\left(Y\in C\wedge \underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}Y/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(Y\in C\wedge \psi \right)\right)$$
55	45 49 54	3bitrd	$$⊢X\in D\to \left(Y\in \left\{w\in ⦋X/x⦌B|\underset{\dot{}}{[}X/x\underset{\dot{}}{]}\underset{\dot{}}{[}w/y\underset{\dot{}}{]}\phi \right\}\leftrightarrow \left(Y\in C\wedge \psi \right)\right)$$
56		3anass	$$⊢\left(X\in D\wedge Y\in C\wedge \psi \right)\leftrightarrow \left(X\in D\wedge \left(Y\in C\wedge \psi \right)\right)$$
57	56	baibr	$$⊢X\in D\to \left(\left(Y\in C\wedge \psi \right)\leftrightarrow \left(X\in D\wedge Y\in C\wedge \psi \right)\right)$$
58	41 55 57	3bitrd	$$⊢X\in D\to \left(Y\in F\left(X\right)\leftrightarrow \left(X\in D\wedge Y\in C\wedge \psi \right)\right)$$
59	5 6 58	pm5.21nii	$$⊢Y\in F\left(X\right)\leftrightarrow \left(X\in D\wedge Y\in C\wedge \psi \right)$$