Theorem elmptrab 21440

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 6198	. 2 ⊢ (𝑌 ∈ (𝐹‘𝑋) → 𝑋 ∈ 𝐷)
3		simp1 1054	. 2 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓) → 𝑋 ∈ 𝐷)
4		csbeq1 3502	. . . . . 6 ⊢ (𝑧 = 𝑋 → ⦋𝑧 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
5		dfsbcq 3404	. . . . . 6 ⊢ (𝑧 = 𝑋 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑))
6	4, 5	rabeqbidv 3168	. . . . 5 ⊢ (𝑧 = 𝑋 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
7		nfcv 2751	. . . . . . 7 ⊢ Ⅎ𝑧{𝑦 ∈ 𝐵 ∣ 𝜑}
8		nfsbc1v 3422	. . . . . . . 8 ⊢ Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
9		nfcsb1v 3515	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵
10	8, 9	nfrab 3100	. . . . . . 7 ⊢ Ⅎ𝑥{𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑}
11		csbeq1a 3508	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
12		sbceq1a 3413	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
13	11, 12	rabeqbidv 3168	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥]𝜑})
14		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑤⦋𝑧 / 𝑥⦌𝐵
15		nfcv 2751	. . . . . . . . 9 ⊢ Ⅎ𝑦⦋𝑧 / 𝑥⦌𝐵
16		nfcv 2751	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝑧
17		nfsbc1v 3422	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
18	16, 17	nfsbc 3424	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
19		nfv 1830	. . . . . . . . 9 ⊢ Ⅎ𝑤[𝑧 / 𝑥]𝜑
20		sbceq1a 3413	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ([𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
21	20	equcoms 1934	. . . . . . . . . 10 ⊢ (𝑤 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
22		sbccom 3476	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
23	21, 22	syl6rbbr 278	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑧 / 𝑥]𝜑))
24	14, 15, 18, 19, 23	cbvrab 3171	. . . . . . . 8 ⊢ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥]𝜑}
25	13, 24	syl6eqr 2662	. . . . . . 7 ⊢ (𝑥 = 𝑧 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
26	7, 10, 25	cbvmpt 4677	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ 𝜑}) = (𝑧 ∈ 𝐷 ↦ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
27	1, 26	eqtri 2632	. . . . 5 ⊢ 𝐹 = (𝑧 ∈ 𝐷 ↦ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
28		nfv 1830	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐷
29	9	nfel1 2765	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉
30	28, 29	nfim 1813	. . . . . . 7 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)
31		eleq1 2676	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
32	11	eleq1d 2672	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝐵 ∈ 𝑉 ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉))
33	31, 32	imbi12d 333	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉) ↔ (𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)))
34		elmptrab.ex	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉)
35	30, 33, 34	chvar 2250	. . . . . 6 ⊢ (𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)
36		rabexg 4739	. . . . . 6 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
37	35, 36	syl 17	. . . . 5 ⊢ (𝑧 ∈ 𝐷 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
38	6, 27, 37	fvmpt3 6195	. . . 4 ⊢ (𝑋 ∈ 𝐷 → (𝐹‘𝑋) = {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
39	38	eleq2d 2673	. . 3 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ (𝐹‘𝑋) ↔ 𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑}))
40		dfsbcq 3404	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ([𝑤 / 𝑦]𝜑 ↔ [𝑌 / 𝑦]𝜑))
41	40	sbcbidv 3457	. . . . . 6 ⊢ (𝑤 = 𝑌 → ([𝑋 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
42	41	elrab 3331	. . . . 5 ⊢ (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
43	42	a1i 11	. . . 4 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
44		nfcvd 2752	. . . . . . 7 ⊢ (𝑋 ∈ 𝐷 → Ⅎ𝑥𝐶)
45		elmptrab.s2	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)
46	44, 45	csbiegf 3523	. . . . . 6 ⊢ (𝑋 ∈ 𝐷 → ⦋𝑋 / 𝑥⦌𝐵 = 𝐶)
47	46	eleq2d 2673	. . . . 5 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ↔ 𝑌 ∈ 𝐶))
48	47	anbi1d 737	. . . 4 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑) ↔ (𝑌 ∈ 𝐶 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
49		nfv 1830	. . . . . 6 ⊢ Ⅎ𝑥𝜓
50		nfv 1830	. . . . . 6 ⊢ Ⅎ𝑦𝜓
51		nfv 1830	. . . . . 6 ⊢ Ⅎ𝑥 𝑌 ∈ 𝐶
52		elmptrab.s1	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓))
53	49, 50, 51, 52	sbc2iegf 3471	. . . . 5 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶) → ([𝑋 / 𝑥][𝑌 / 𝑦]𝜑 ↔ 𝜓))
54	53	pm5.32da 671	. . . 4 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ 𝐶 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑) ↔ (𝑌 ∈ 𝐶 ∧ 𝜓)))
55	43, 48, 54	3bitrd 293	. . 3 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ 𝐶 ∧ 𝜓)))
56		3anass 1035	. . . 4 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓) ↔ (𝑋 ∈ 𝐷 ∧ (𝑌 ∈ 𝐶 ∧ 𝜓)))
57	56	baibr 943	. . 3 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ 𝐶 ∧ 𝜓) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓)))
58	39, 55, 57	3bitrd 293	. 2 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓)))
59	2, 3, 58	pm5.21nii 367	1 ⊢ (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  {crab 2900  Vcvv 3173  [wsbc 3402  ⦋csb 3499   ↦ cmpt 4643  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fv 5812

This theorem is referenced by:  elmptrab2OLD  21441  elmptrab2  21442  isfbas  21443