Theorem elmptrab

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

	Ref	Expression
Hypotheses	elmptrab.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
	elmptrab.s1	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) )
	elmptrab.s2	⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
	elmptrab.ex	⊢ ( 𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉 )
Assertion	elmptrab	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		elmptrab.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } )
2		elmptrab.s1	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝜑 ↔ 𝜓 ) )
3		elmptrab.s2	⊢ ( 𝑥 = 𝑋 → 𝐵 = 𝐶 )
4		elmptrab.ex	⊢ ( 𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉 )
5	1	mptrcl	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) → 𝑋 ∈ 𝐷 )
6		simp1	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) → 𝑋 ∈ 𝐷 )
7		csbeq1	⊢ ( 𝑧 = 𝑋 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
8		dfsbcq	⊢ ( 𝑧 = 𝑋 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) )
9	7 8	rabeqbidv	⊢ ( 𝑧 = 𝑋 → { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } = { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
10		nfcv	⊢ Ⅎ 𝑧 { 𝑦 ∈ 𝐵 ∣ 𝜑 }
11		nfsbc1v	⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑
12		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
13	11 12	nfrabw	⊢ Ⅎ 𝑥 { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 }
14		csbeq1a	⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
15		sbceq1a	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
16	14 15	rabeqbidv	⊢ ( 𝑥 = 𝑧 → { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] 𝜑 } )
17		nfcv	⊢ Ⅎ 𝑤 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
18		nfcv	⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
19		nfcv	⊢ Ⅎ 𝑦 𝑧
20		nfsbc1v	⊢ Ⅎ 𝑦 [ 𝑤 / 𝑦 ] 𝜑
21	19 20	nfsbcw	⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑
22		nfv	⊢ Ⅎ 𝑤 [ 𝑧 / 𝑥 ] 𝜑
23		sbceq1a	⊢ ( 𝑦 = 𝑤 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ) )
24	23	equcoms	⊢ ( 𝑤 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 ) )
25		sbccom	⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 )
26	24 25	syl6rbbr	⊢ ( 𝑤 = 𝑦 → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] 𝜑 ) )
27	17 18 21 22 26	cbvrabw	⊢ { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } = { 𝑦 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] 𝜑 }
28	16 27	eqtr4di	⊢ ( 𝑥 = 𝑧 → { 𝑦 ∈ 𝐵 ∣ 𝜑 } = { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
29	10 13 28	cbvmpt	⊢ ( 𝑥 ∈ 𝐷 ↦ { 𝑦 ∈ 𝐵 ∣ 𝜑 } ) = ( 𝑧 ∈ 𝐷 ↦ { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
30	1 29	eqtri	⊢ 𝐹 = ( 𝑧 ∈ 𝐷 ↦ { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
31		nfv	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐷
32	12	nfel1	⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉
33	31 32	nfim	⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐷 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
34		eleq1w	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷 ) )
35	14	eleq1d	⊢ ( 𝑥 = 𝑧 → ( 𝐵 ∈ 𝑉 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) )
36	34 35	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉 ) ↔ ( 𝑧 ∈ 𝐷 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) ) )
37	33 36 4	chvarfv	⊢ ( 𝑧 ∈ 𝐷 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
38		rabexg	⊢ ( ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∈ 𝑉 → { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ∈ V )
39	37 38	syl	⊢ ( 𝑧 ∈ 𝐷 → { 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ∣ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ∈ V )
40	9 30 39	fvmpt3	⊢ ( 𝑋 ∈ 𝐷 → ( 𝐹 ‘ 𝑋 ) = { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } )
41	40	eleq2d	⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ 𝑌 ∈ { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ) )
42		dfsbcq	⊢ ( 𝑤 = 𝑌 → ( [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑌 / 𝑦 ] 𝜑 ) )
43	42	sbcbidv	⊢ ( 𝑤 = 𝑌 → ( [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
44	43	elrab	⊢ ( 𝑌 ∈ { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ↔ ( 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∧ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) )
45	44	a1i	⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ↔ ( 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∧ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ) )
46		nfcvd	⊢ ( 𝑋 ∈ 𝐷 → Ⅎ 𝑥 𝐶 )
47	46 3	csbiegf	⊢ ( 𝑋 ∈ 𝐷 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 = 𝐶 )
48	47	eleq2d	⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ↔ 𝑌 ∈ 𝐶 ) )
49	48	anbi1d	⊢ ( 𝑋 ∈ 𝐷 → ( ( 𝑌 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∧ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ↔ ( 𝑌 ∈ 𝐶 ∧ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ) )
50		nfv	⊢ Ⅎ 𝑥 𝜓
51		nfv	⊢ Ⅎ 𝑦 𝜓
52		nfv	⊢ Ⅎ 𝑥 𝑌 ∈ 𝐶
53	50 51 52 2	sbc2iegf	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ) → ( [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ↔ 𝜓 ) )
54	53	pm5.32da	⊢ ( 𝑋 ∈ 𝐷 → ( ( 𝑌 ∈ 𝐶 ∧ [ 𝑋 / 𝑥 ] [ 𝑌 / 𝑦 ] 𝜑 ) ↔ ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) ) )
55	45 49 54	3bitrd	⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ { 𝑤 ∈ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∣ [ 𝑋 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 } ↔ ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) ) )
56		3anass	⊢ ( ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) ↔ ( 𝑋 ∈ 𝐷 ∧ ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) ) )
57	56	baibr	⊢ ( 𝑋 ∈ 𝐷 → ( ( 𝑌 ∈ 𝐶 ∧ 𝜓 ) ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) ) )
58	41 55 57	3bitrd	⊢ ( 𝑋 ∈ 𝐷 → ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) ) )
59	5 6 58	pm5.21nii	⊢ ( 𝑌 ∈ ( 𝐹 ‘ 𝑋 ) ↔ ( 𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓 ) )