Theorem elmptrab 24176

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 7026	. 2 ⊢ (𝑌 ∈ (𝐹‘𝑋) → 𝑋 ∈ 𝐷)
3		simp1 1154	. 2 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓) → 𝑋 ∈ 𝐷)
4		csbeq1 3854	. . . . . 6 ⊢ (𝑧 = 𝑋 → ⦋𝑧 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
5		dfsbcq 3744	. . . . . 6 ⊢ (𝑧 = 𝑋 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑))
6	4, 5	rabeqbidv 3433	. . . . 5 ⊢ (𝑧 = 𝑋 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
7		nfcv 2926	. . . . . . 7 ⊢ Ⅎ𝑧{𝑦 ∈ 𝐵 ∣ 𝜑}
8		nfsbc1v 3762	. . . . . . . 8 ⊢ Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
9		nfcsb1v 3875	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵
10	8, 9	nfrabw 3451	. . . . . . 7 ⊢ Ⅎ𝑥{𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑}
11		csbeq1a 3865	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
12		sbceq1a 3753	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
13	11, 12	rabeqbidv 3433	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥]𝜑})
14		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑤⦋𝑧 / 𝑥⦌𝐵
15		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑦⦋𝑧 / 𝑥⦌𝐵
16		nfcv 2926	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝑧
17		nfsbc1v 3762	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
18	16, 17	nfsbcw 3764	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
19		nfv 1949	. . . . . . . . 9 ⊢ Ⅎ𝑤[𝑧 / 𝑥]𝜑
20		sbccom 3822	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
21		sbceq1a 3753	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ([𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
22	21	equcoms 2055	. . . . . . . . . 10 ⊢ (𝑤 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
23	20, 22	bitr4id 293	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑧 / 𝑥]𝜑))
24	14, 15, 18, 19, 23	cbvrabw 3450	. . . . . . . 8 ⊢ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥]𝜑}
25	13, 24	eqtr4di 2816	. . . . . . 7 ⊢ (𝑥 = 𝑧 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
26	7, 10, 25	cbvmpt 5210	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ 𝜑}) = (𝑧 ∈ 𝐷 ↦ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
27	1, 26	eqtri 2786	. . . . 5 ⊢ 𝐹 = (𝑧 ∈ 𝐷 ↦ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
28		nfv 1949	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐷
29	9	nfel1 2942	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉
30	28, 29	nfim 1931	. . . . . . 7 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)
31		eleq1w 2847	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
32	11	eleq1d 2849	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝐵 ∈ 𝑉 ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉))
33	31, 32	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉) ↔ (𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)))
34		elmptrab.ex	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉)
35	30, 33, 34	chvarfv 2280	. . . . . 6 ⊢ (𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)
36		rabexg 5303	. . . . . 6 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
37	35, 36	syl 18	. . . . 5 ⊢ (𝑧 ∈ 𝐷 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
38	6, 27, 37	fvmpt3 7021	. . . 4 ⊢ (𝑋 ∈ 𝐷 → (𝐹‘𝑋) = {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
39	38	eleq2d 2850	. . 3 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ (𝐹‘𝑋) ↔ 𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑}))
40		dfsbcq 3744	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ([𝑤 / 𝑦]𝜑 ↔ [𝑌 / 𝑦]𝜑))
41	40	sbcbidv 3797	. . . . . 6 ⊢ (𝑤 = 𝑌 → ([𝑋 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
42	41	elrab 3648	. . . . 5 ⊢ (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
43	42	a1i 11	. . . 4 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
44		nfcvd 2927	. . . . . . 7 ⊢ (𝑋 ∈ 𝐷 → Ⅎ𝑥𝐶)
45		elmptrab.s2	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)
46	44, 45	csbiegf 3884	. . . . . 6 ⊢ (𝑋 ∈ 𝐷 → ⦋𝑋 / 𝑥⦌𝐵 = 𝐶)
47	46	eleq2d 2850	. . . . 5 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ↔ 𝑌 ∈ 𝐶))
48	47	anbi1d 643	. . . 4 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑) ↔ (𝑌 ∈ 𝐶 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
49		nfv 1949	. . . . . 6 ⊢ Ⅎ𝑥𝜓
50		nfv 1949	. . . . . 6 ⊢ Ⅎ𝑦𝜓
51		nfv 1949	. . . . . 6 ⊢ Ⅎ𝑥 𝑌 ∈ 𝐶
52		elmptrab.s1	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓))
53	49, 50, 51, 52	sbc2iegf 3817	. . . . 5 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶) → ([𝑋 / 𝑥][𝑌 / 𝑦]𝜑 ↔ 𝜓))
54	53	pm5.32da 590	. . . 4 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ 𝐶 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑) ↔ (𝑌 ∈ 𝐶 ∧ 𝜓)))
55	43, 48, 54	3bitrd 308	. . 3 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ 𝐶 ∧ 𝜓)))
56		3anass 1111	. . . 4 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓) ↔ (𝑋 ∈ 𝐷 ∧ (𝑌 ∈ 𝐶 ∧ 𝜓)))
57	56	baibr 546	. . 3 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ 𝐶 ∧ 𝜓) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓)))
58	39, 55, 57	3bitrd 308	. 2 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓)))
59	2, 3, 58	pm5.21nii 381	1 ⊢ (𝑌 ∈ (𝐹‘𝑋) ↔ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  {crab 3416  Vcvv 3454  [wsbc 3742  ⦋csb 3851   ↦ cmpt 5189  ‘cfv 6558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6512  df-fun 6560  df-fv 6566

This theorem is used by:  elmptrab2  24177  isfbas  24178