Theorem reusv2 5358

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 3426	. . . 4 ⊢ Ⅎ𝑦{𝑦 ∈ 𝐵 ∣ 𝜑}
2		nfcv 2891	. . . 4 ⊢ Ⅎ𝑧{𝑦 ∈ 𝐵 ∣ 𝜑}
3		nfv 1914	. . . 4 ⊢ Ⅎ𝑧 𝐶 ∈ 𝐴
4		nfcsb1v 3886	. . . . 5 ⊢ Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐶
5	4	nfel1 2908	. . . 4 ⊢ Ⅎ𝑦⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴
6		csbeq1a 3876	. . . . 5 ⊢ (𝑦 = 𝑧 → 𝐶 = ⦋𝑧 / 𝑦⦌𝐶)
7	6	eleq1d 2813	. . . 4 ⊢ (𝑦 = 𝑧 → (𝐶 ∈ 𝐴 ↔ ⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴))
8	1, 2, 3, 5, 7	cbvralfw 3278	. . 3 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝐶 ∈ 𝐴 ↔ ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴)
9		rabid 3427	. . . . . 6 ⊢ (𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ↔ (𝑦 ∈ 𝐵 ∧ 𝜑))
10	9	imbi1i 349	. . . . 5 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝐶 ∈ 𝐴) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐶 ∈ 𝐴))
11		impexp 450	. . . . 5 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝐶 ∈ 𝐴) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝐶 ∈ 𝐴)))
12	10, 11	bitri 275	. . . 4 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝐶 ∈ 𝐴) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝐶 ∈ 𝐴)))
13	12	ralbii2 3071	. . 3 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝐶 ∈ 𝐴 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴))
14	8, 13	bitr3i 277	. 2 ⊢ (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴))
15		rabn0 4352	. 2 ⊢ ({𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅ ↔ ∃𝑦 ∈ 𝐵 𝜑)
16		reusv2lem5 5357	. . 3 ⊢ ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶))
17		nfv 1914	. . . . . 6 ⊢ Ⅎ𝑧 𝑥 = 𝐶
18	4	nfeq2 2909	. . . . . 6 ⊢ Ⅎ𝑦 𝑥 = ⦋𝑧 / 𝑦⦌𝐶
19	6	eqeq2d 2740	. . . . . 6 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝐶 ↔ 𝑥 = ⦋𝑧 / 𝑦⦌𝐶))
20	1, 2, 17, 18, 19	cbvrexfw 3279	. . . . 5 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶)
21	9	anbi1i 624	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ∧ 𝑥 = 𝐶) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) ∧ 𝑥 = 𝐶))
22		anass 468	. . . . . . 7 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) ∧ 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ (𝜑 ∧ 𝑥 = 𝐶)))
23	21, 22	bitri 275	. . . . . 6 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} ∧ 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 ∧ (𝜑 ∧ 𝑥 = 𝐶)))
24	23	rexbii2 3072	. . . . 5 ⊢ (∃𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶))
25	20, 24	bitr3i 277	. . . 4 ⊢ (∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶))
26	25	reubii 3363	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∃𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶))
27	1, 2, 17, 18, 19	cbvralfw 3278	. . . . 5 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶)
28	9	imbi1i 349	. . . . . . 7 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 = 𝐶) ↔ ((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝑥 = 𝐶))
29		impexp 450	. . . . . . 7 ⊢ (((𝑦 ∈ 𝐵 ∧ 𝜑) → 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝑥 = 𝐶)))
30	28, 29	bitri 275	. . . . . 6 ⊢ ((𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑} → 𝑥 = 𝐶) ↔ (𝑦 ∈ 𝐵 → (𝜑 → 𝑥 = 𝐶)))
31	30	ralbii2 3071	. . . . 5 ⊢ (∀𝑦 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = 𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))
32	27, 31	bitr3i 277	. . . 4 ⊢ (∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))
33	32	reubii 3363	. . 3 ⊢ (∃!𝑥 ∈ 𝐴 ∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}𝑥 = ⦋𝑧 / 𝑦⦌𝐶 ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶))
34	16, 26, 33	3bitr3g 313	. 2 ⊢ ((∀𝑧 ∈ {𝑦 ∈ 𝐵 ∣ 𝜑}⦋𝑧 / 𝑦⦌𝐶 ∈ 𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝜑} ≠ ∅) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))
35	14, 15, 34	syl2anbr 599	1 ⊢ ((∀𝑦 ∈ 𝐵 (𝜑 → 𝐶 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐵 𝜑) → (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝑥 = 𝐶) ↔ ∃!𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 → 𝑥 = 𝐶)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ≠ wne 2925  ∀wral 3044  ∃wrex 3053  ∃!wreu 3352  {crab 3405  ⦋csb 3862  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-nul 5261  ax-pow 5320

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-nul 4297

This theorem is referenced by:  cdleme25dN  40350