Theorem elmptrab 24054

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 7000	. 2 ⊢ (𝑌 ∈ (𝐹‘𝑋) → 𝑋 ∈ 𝐷)
3		simp1 1154	. 2 ⊢ ((𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐶 ∧ 𝜓) → 𝑋 ∈ 𝐷)
4		csbeq1 3853	. . . . . 6 ⊢ (𝑧 = 𝑋 → ⦋𝑧 / 𝑥⦌𝐵 = ⦋𝑋 / 𝑥⦌𝐵)
5		dfsbcq 3744	. . . . . 6 ⊢ (𝑧 = 𝑋 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑))
6	4, 5	rabeqbidv 3432	. . . . 5 ⊢ (𝑧 = 𝑋 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
7		nfcv 2924	. . . . . . 7 ⊢ Ⅎ𝑧{𝑦 ∈ 𝐵 ∣ 𝜑}
8		nfsbc1v 3762	. . . . . . . 8 ⊢ Ⅎ𝑥[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
9		nfcsb1v 3874	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵
10	8, 9	nfrabw 3450	. . . . . . 7 ⊢ Ⅎ𝑥{𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑}
11		csbeq1a 3864	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵)
12		sbceq1a 3753	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑))
13	11, 12	rabeqbidv 3432	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥]𝜑})
14		nfcv 2924	. . . . . . . . 9 ⊢ Ⅎ𝑤⦋𝑧 / 𝑥⦌𝐵
15		nfcv 2924	. . . . . . . . 9 ⊢ Ⅎ𝑦⦋𝑧 / 𝑥⦌𝐵
16		nfcv 2924	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝑧
17		nfsbc1v 3762	. . . . . . . . . 10 ⊢ Ⅎ𝑦[𝑤 / 𝑦]𝜑
18	16, 17	nfsbcw 3764	. . . . . . . . 9 ⊢ Ⅎ𝑦[𝑧 / 𝑥][𝑤 / 𝑦]𝜑
19		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑤[𝑧 / 𝑥]𝜑
20		sbccom 3821	. . . . . . . . . 10 ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)
21		sbceq1a 3753	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑤 → ([𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
22	21	equcoms 2053	. . . . . . . . . 10 ⊢ (𝑤 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑))
23	20, 22	bitr4id 293	. . . . . . . . 9 ⊢ (𝑤 = 𝑦 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑧 / 𝑥]𝜑))
24	14, 15, 18, 19, 23	cbvrabw 3449	. . . . . . . 8 ⊢ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} = {𝑦 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥]𝜑}
25	13, 24	eqtr4di 2815	. . . . . . 7 ⊢ (𝑥 = 𝑧 → {𝑦 ∈ 𝐵 ∣ 𝜑} = {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
26	7, 10, 25	cbvmpt 5211	. . . . . 6 ⊢ (𝑥 ∈ 𝐷 ↦ {𝑦 ∈ 𝐵 ∣ 𝜑}) = (𝑧 ∈ 𝐷 ↦ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
27	1, 26	eqtri 2785	. . . . 5 ⊢ 𝐹 = (𝑧 ∈ 𝐷 ↦ {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑})
28		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐷
29	9	nfel1 2940	. . . . . . . 8 ⊢ Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉
30	28, 29	nfim 1929	. . . . . . 7 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)
31		eleq1w 2845	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐷 ↔ 𝑧 ∈ 𝐷))
32	11	eleq1d 2847	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (𝐵 ∈ 𝑉 ↔ ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉))
33	31, 32	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉) ↔ (𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)))
34		elmptrab.ex	. . . . . . 7 ⊢ (𝑥 ∈ 𝐷 → 𝐵 ∈ 𝑉)
35	30, 33, 34	chvarfv 2278	. . . . . 6 ⊢ (𝑧 ∈ 𝐷 → ⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉)
36		rabexg 5306	. . . . . 6 ⊢ (⦋𝑧 / 𝑥⦌𝐵 ∈ 𝑉 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
37	35, 36	syl 18	. . . . 5 ⊢ (𝑧 ∈ 𝐷 → {𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐵 ∣ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑} ∈ V)
38	6, 27, 37	fvmpt3 6995	. . . 4 ⊢ (𝑋 ∈ 𝐷 → (𝐹‘𝑋) = {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑})
39	38	eleq2d 2848	. . 3 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ (𝐹‘𝑋) ↔ 𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑}))
40		dfsbcq 3744	. . . . . . 7 ⊢ (𝑤 = 𝑌 → ([𝑤 / 𝑦]𝜑 ↔ [𝑌 / 𝑦]𝜑))
41	40	sbcbidv 3797	. . . . . 6 ⊢ (𝑤 = 𝑌 → ([𝑋 / 𝑥][𝑤 / 𝑦]𝜑 ↔ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
42	41	elrab 3648	. . . . 5 ⊢ (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑))
43	42	a1i 11	. . . 4 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ {𝑤 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∣ [𝑋 / 𝑥][𝑤 / 𝑦]𝜑} ↔ (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
44		nfcvd 2925	. . . . . . 7 ⊢ (𝑋 ∈ 𝐷 → Ⅎ𝑥𝐶)
45		elmptrab.s2	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝐵 = 𝐶)
46	44, 45	csbiegf 3883	. . . . . 6 ⊢ (𝑋 ∈ 𝐷 → ⦋𝑋 / 𝑥⦌𝐵 = 𝐶)
47	46	eleq2d 2848	. . . . 5 ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ↔ 𝑌 ∈ 𝐶))
48	47	anbi1d 643	. . . 4 ⊢ (𝑋 ∈ 𝐷 → ((𝑌 ∈ ⦋𝑋 / 𝑥⦌𝐵 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑) ↔ (𝑌 ∈ 𝐶 ∧ [𝑋 / 𝑥][𝑌 / 𝑦]𝜑)))
49		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑥𝜓
50		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑦𝜓
51		nfv 1947	. . . . . 6 ⊢ Ⅎ𝑥 𝑌 ∈ 𝐶
52		elmptrab.s1	. . . . . 6 ⊢ ((𝑥 = 𝑋 ∧ 𝑦 = 𝑌) → (𝜑 ↔ 𝜓))
53	49, 50, 51, 52	sbc2iegf 3816	. . . . 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 2145  {crab 3414  Vcvv 3453  [wsbc 3742  ⦋csb 3850   ↦ cmpt 5190  ‘cfv 6537

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is used by:  elmptrab2  24055  isfbas  24056