Theorem reusv2 5321

Description: Two ways to express single-valuedness of a class expression 𝐶(𝑦) that is constant for those 𝑦 ∈ 𝐵 such that 𝜑. The first antecedent ensures that the constant value belongs to the existential uniqueness domain 𝐴, and the second ensures that 𝐶(𝑦) is evaluated for at least one 𝑦. (Contributed by NM, 4-Jan-2013.) (Proof shortened by Mario Carneiro, 19-Nov-2016.)

Assertion

Ref	Expression
reusv2	⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐵 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵   𝑥,𝐶   𝜑,𝑥

Allowed substitution hints:   𝜑(𝑦)   𝐵(𝑦)   𝐶(𝑦)

Proof of Theorem reusv2

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfrab1 3310	. . . 4 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝜑}
2		nfcv 2906	. . . 4 ⊢ Ⅎ𝑧{𝑦 ∈ 𝐵 ∣ 𝜑}
3		nfv 1918	. . . 4 ⊢ Ⅎ𝑧 𝐶 ∈ 𝐴
4		nfcsb1v 3853	. . . . 5 ⊢ Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐶
5	4	nfel1 2922	. . . 4 ⊢ Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴
6		csbeq1a 3842	. . . . 5 ⊢ (𝑦 = 𝑧 → 𝐶 = ⦋𝑧 / 𝑦⦌𝐶)
7	6	eleq1d 2823	. . . 4 ⊢ (𝑦 = 𝑧 → (𝐶 ∈ 𝐴 ↔ ⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴))
8	1, 2, 3, 5, 7	cbvralfw 3358	. . 3 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝐶 ∈ 𝐴 ↔ ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴)
9		rabid 3304	. . . . . 6 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ (𝑦 ∈ 𝐵 ∧ 𝜑))
10	9	imbi1i 349	. . . . 5 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝐶 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐶 ∈ 𝐴))
11		impexp 450	. . . . 5 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐶 ∈ 𝐴) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝐶 ∈ 𝐴)))
12	10, 11	bitri 274	. . . 4 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝐶 ∈ 𝐴) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝐶 ∈ 𝐴)))
13	12	ralbii2 3088	. . 3 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝐶 ∈ 𝐴 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴))
14	8, 13	bitr3i 276	. 2 ⊢ (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴))
15		rabn0 4316	. 2 ⊢ ({𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅ ↔ ∃𝑦 ∈ 𝐵 𝜑)
16		reusv2lem5 5320	. . 3 ⊢ ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶))
17		nfv 1918	. . . . . 6 ⊢ Ⅎ𝑧 𝑥 = 𝐶
18	4	nfeq2 2923	. . . . . 6 ⊢ Ⅎ𝑦 𝑥 = ⦋𝑧 / 𝑦⦌𝐶
19	6	eqeq2d 2749	. . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝐶 ↔ 𝑥 = ⦋𝑧 / 𝑦⦌𝐶))
20	1, 2, 17, 18, 19	cbvrexfw 3360	. . . . 5 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶)
21	9	anbi1i 623	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ∧ 𝑥 = 𝐶) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) ∧ 𝑥 = 𝐶))
22		anass 468	. . . . . . 7 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) ∧ 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ (𝜑 ∧ 𝑥 = 𝐶)))
23	21, 22	bitri 274	. . . . . 6 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ∧ 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ (𝜑 ∧ 𝑥 = 𝐶)))
24	23	rexbii2 3175	. . . . 5 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶))
25	20, 24	bitr3i 276	. . . 4 ⊢ (∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶))
26	25	reubii 3317	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶))
27	1, 2, 17, 18, 19	cbvralfw 3358	. . . . 5 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶)
28	9	imbi1i 349	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 = 𝐶) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝑥 = 𝐶))
29		impexp 450	. . . . . . 7 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝑥 = 𝐶)))
30	28, 29	bitri 274	. . . . . 6 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝑥 = 𝐶)))
31	30	ralbii2 3088	. . . . 5 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))
32	27, 31	bitr3i 276	. . . 4 ⊢ (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))
33	32	reubii 3317	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))
34	16, 26, 33	3bitr3g 312	. 2 ⊢ ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))
35	14, 15, 34	syl2anbr 598	1 ⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐵 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ∀wral 3063  ∃wrex 3064  ∃!wreu 3065  {crab 3067  ⦋csb 3828  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225  ax-pow 5283

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-nul 4254

This theorem is referenced by:  cdleme25dN  38297