Theorem elmptrab 23076

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

Hypotheses

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

Assertion

Ref	Expression
elmptrab	⊢ (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓))

Distinct variable groups:   𝑥,𝑦,𝑋   𝑦,𝐵   𝑥,𝐶,𝑦   𝑥,𝐷   𝑥,𝑉,𝑦   𝑥,𝑌,𝑦   𝜓,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐵(𝑥)   𝐷(𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem elmptrab

Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elmptrab.f	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ 𝜑})
2	1	mptrcl 6934	. 2 ⊢ (𝑌 ∈ (𝐹‘𝑋) → 𝑋 ∈ 𝐷)
3		simp1 1135	. 2 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓) → 𝑋 ∈ 𝐷)
4		csbeq1 3845	. . . . . 6 ⊢ (𝑧 = 𝑋 → ⦋𝑧 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
5		dfsbcq 3728	. . . . . 6 ⊢ (𝑧 = 𝑋 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑))
6	4, 5	rabeqbidv 3420	. . . . 5 ⊢ (𝑧 = 𝑋 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
7		nfcv 2904	. . . . . . 7 ⊢ Ⅎ𝑧{𝑦 ∈ 𝐵 ∣ 𝜑}
8		nfsbc1v 3746	. . . . . . . 8 ⊢ Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
9		nfcsb1v 3867	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵
10	8, 9	nfrabw 3436	. . . . . . 7 ⊢ Ⅎ𝑥{𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑}
11		csbeq1a 3856	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
12		sbceq1a 3737	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
13	11, 12	rabeqbidv 3420	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥]𝜑})
14		nfcv 2904	. . . . . . . . 9 ⊢ Ⅎ𝑤⦋𝑧 / 𝑥⦌𝐵
15		nfcv 2904	. . . . . . . . 9 ⊢ Ⅎ𝑦⦋𝑧 / 𝑥⦌𝐵
16		nfcv 2904	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝑧
17		nfsbc1v 3746	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
18	16, 17	nfsbcw 3748	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
19		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑤[𝑧 / 𝑥]𝜑
20		sbccom 3814	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
21		sbceq1a 3737	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ([𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
22	21	equcoms 2022	. . . . . . . . . 10 ⊢ (𝑤 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
23	20, 22	bitr4id 289	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑧 / 𝑥]𝜑))
24	14, 15, 18, 19, 23	cbvrabw 3435	. . . . . . . 8 ⊢ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥]𝜑}
25	13, 24	eqtr4di 2794	. . . . . . 7 ⊢ (𝑥 = 𝑧 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
26	7, 10, 25	cbvmpt 5200	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ 𝜑}) = (𝑧 ∈ 𝐷 ↦ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
27	1, 26	eqtri 2764	. . . . 5 ⊢ 𝐹 = (𝑧 ∈ 𝐷 ↦ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
28		nfv 1916	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐷
29	9	nfel1 2920	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉
30	28, 29	nfim 1898	. . . . . . 7 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)
31		eleq1w 2819	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
32	11	eleq1d 2821	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝐵 ∈ 𝑉 ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉))
33	31, 32	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉) ↔ (𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)))
34		elmptrab.ex	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉)
35	30, 33, 34	chvarfv 2232	. . . . . 6 ⊢ (𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)
36		rabexg 5272	. . . . . 6 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
37	35, 36	syl 17	. . . . 5 ⊢ (𝑧 ∈ 𝐷 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
38	6, 27, 37	fvmpt3 6929	. . . 4 ⊢ (𝑋 ∈ 𝐷 → (𝐹‘𝑋) = {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
39	38	eleq2d 2822	. . 3 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ (𝐹‘𝑋) ↔ 𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑}))
40		dfsbcq 3728	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ([𝑤 / 𝑦]𝜑 ↔ [𝑌 / 𝑦]𝜑))
41	40	sbcbidv 3785	. . . . . 6 ⊢ (𝑤 = 𝑌 → ([𝑋 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
42	41	elrab 3634	. . . . 5 ⊢ (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
43	42	a1i 11	. . . 4 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
44		nfcvd 2905	. . . . . . 7 ⊢ (𝑋 ∈ 𝐷 → Ⅎ𝑥𝐶)
45		elmptrab.s2	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)
46	44, 45	csbiegf 3876	. . . . . 6 ⊢ (𝑋 ∈ 𝐷 → ⦋𝑋 / 𝑥⦌𝐵 = 𝐶)
47	46	eleq2d 2822	. . . . 5 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ↔ 𝑌 ∈ 𝐶))
48	47	anbi1d 630	. . . 4 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑) ↔ (𝑌 ∈ 𝐶 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
49		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑥𝜓
50		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑦𝜓
51		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑥 𝑌 ∈ 𝐶
52		elmptrab.s1	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓))
53	49, 50, 51, 52	sbc2iegf 3808	. . . . 5 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶) → ([𝑋 / 𝑥][𝑌 / 𝑦]𝜑 ↔ 𝜓))
54	53	pm5.32da 579	. . . 4 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ 𝐶 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑) ↔ (𝑌 ∈ 𝐶 ∧ 𝜓)))
55	43, 48, 54	3bitrd 304	. . 3 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ 𝐶 ∧ 𝜓)))
56		3anass 1094	. . . 4 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓) ↔ (𝑋 ∈ 𝐷 ∧ (𝑌 ∈ 𝐶 ∧ 𝜓)))
57	56	baibr 537	. . 3 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ 𝐶 ∧ 𝜓) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓)))
58	39, 55, 57	3bitrd 304	. 2 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓)))
59	2, 3, 58	pm5.21nii 379	1 ⊢ (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  {crab 3403  Vcvv 3441  [wsbc 3726  ⦋csb 3842   ↦ cmpt 5172  ‘cfv 6473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pr 5369

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-mpt 5173  df-id 5512  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6425  df-fun 6475  df-fv 6481

This theorem is referenced by:  elmptrab2  23077  isfbas  23078