Theorem unirep 35608

Description: Define a quantity whose definition involves a choice of representative, but which is uniquely determined regardless of the choice. (Contributed by Jeff Madsen, 1-Jun-2011.)

Hypotheses

Ref	Expression
unirep.1	⊢ (𝑦 = 𝐷 → (𝜑 ↔ 𝜓))
unirep.2	⊢ (𝑦 = 𝐷 → 𝐵 = 𝐶)
unirep.3	⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))
unirep.4	⊢ (𝑦 = 𝑧 → 𝐵 = 𝐹)
unirep.5	⊢ 𝐵 ∈ V

Assertion

Ref	Expression
unirep	⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶)

Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑧   𝑥,𝐶,𝑦   𝑥,𝐷,𝑦   𝑥,𝐹,𝑦   𝜑,𝑥,𝑧   𝜓,𝑥,𝑦   𝜒,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑧)   𝜒(𝑧)   𝐵(𝑦)   𝐶(𝑧)   𝐷(𝑧)   𝐹(𝑧)

Proof of Theorem unirep

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2738	. . . . 5 ⊢ (𝜓 → 𝐶 = 𝐶)
2	1	ancli 552	. . . 4 ⊢ (𝜓 → (𝜓 ∧ 𝐶 = 𝐶))
3		unirep.1	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝜑 ↔ 𝜓))
4		unirep.2	. . . . . . 7 ⊢ (𝑦 = 𝐷 → 𝐵 = 𝐶)
5	4	eqeq2d 2748	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝐶 = 𝐵 ↔ 𝐶 = 𝐶))
6	3, 5	anbi12d 634	. . . . 5 ⊢ (𝑦 = 𝐷 → ((𝜑 ∧ 𝐶 = 𝐵) ↔ (𝜓 ∧ 𝐶 = 𝐶)))
7	6	rspcev 3537	. . . 4 ⊢ ((𝐷 ∈ 𝐴 ∧ (𝜓 ∧ 𝐶 = 𝐶)) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
8	2, 7	sylan2 596	. . 3 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
9	8	adantl 485	. 2 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
10		nfcvd 2905	. . . . . 6 ⊢ (𝐷 ∈ 𝐴 → Ⅎ𝑦𝐶)
11	10, 4	csbiegf 3845	. . . . 5 ⊢ (𝐷 ∈ 𝐴 → ⦋𝐷 / 𝑦⦌𝐵 = 𝐶)
12		unirep.5	. . . . . 6 ⊢ 𝐵 ∈ V
13	12	csbex 5204	. . . . 5 ⊢ ⦋𝐷 / 𝑦⦌𝐵 ∈ V
14	11, 13	eqeltrrdi 2847	. . . 4 ⊢ (𝐷 ∈ 𝐴 → 𝐶 ∈ V)
15	14	ad2antrl 728	. . 3 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → 𝐶 ∈ V)
16		eqeq1 2741	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐶 → (𝑥 = 𝐵 ↔ 𝐶 = 𝐵))
17	16	anbi2d 632	. . . . . . . . . 10 ⊢ (𝑥 = 𝐶 → ((𝜑 ∧ 𝑥 = 𝐵) ↔ (𝜑 ∧ 𝐶 = 𝐵)))
18	17	rexbidv 3216	. . . . . . . . 9 ⊢ (𝑥 = 𝐶 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵)))
19	18	spcegv 3512	. . . . . . . 8 ⊢ (𝐶 ∈ V → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)))
20	14, 19	syl 17	. . . . . . 7 ⊢ (𝐷 ∈ 𝐴 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)))
21	20	adantr 484	. . . . . 6 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)))
22	8, 21	mpd 15	. . . . 5 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))
23	22	adantl 485	. . . 4 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))
24		r19.29 3176	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → ∃𝑦 ∈ 𝐴 (∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)))
25		r19.29 3176	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → ∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)))
26		an4 656	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 = 𝐵) ∧ (𝜒 ∧ 𝑤 = 𝐹)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝑥 = 𝐵 ∧ 𝑤 = 𝐹)))
27		pm3.35 803	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹)) → 𝐵 = 𝐹)
28		eqeq12 2754	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → (𝑥 = 𝑤 ↔ 𝐵 = 𝐹))
29	27, 28	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹)) → ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
30	29	ancoms 462	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝜒)) → ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
31	30	expimpd 457	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜑 ∧ 𝜒) ∧ (𝑥 = 𝐵 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
32	26, 31	syl5bi 245	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜑 ∧ 𝑥 = 𝐵) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
33	32	ancomsd 469	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜒 ∧ 𝑤 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤))
34	33	expdimp 456	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝑤))
35	34	rexlimivw 3201	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝑤))
36	35	imp 410	. . . . . . . . . . . 12 ⊢ ((∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤)
37	25, 36	sylan 583	. . . . . . . . . . 11 ⊢ (((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤)
38	37	an32s 652	. . . . . . . . . 10 ⊢ (((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)
39	38	ex 416	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
40	39	rexlimivw 3201	. . . . . . . 8 ⊢ (∃𝑦 ∈ 𝐴 (∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
41	24, 40	syl 17	. . . . . . 7 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
42	41	expimpd 457	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → ((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
43	42	adantr 484	. . . . 5 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
44	43	alrimivv 1936	. . . 4 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∀𝑥∀𝑤((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
45		eqeq1 2741	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝐵 ↔ 𝑤 = 𝐵))
46	45	anbi2d 632	. . . . . . 7 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 = 𝐵) ↔ (𝜑 ∧ 𝑤 = 𝐵)))
47	46	rexbidv 3216	. . . . . 6 ⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑤 = 𝐵)))
48		unirep.3	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))
49		unirep.4	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → 𝐵 = 𝐹)
50	49	eqeq2d 2748	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝑤 = 𝐵 ↔ 𝑤 = 𝐹))
51	48, 50	anbi12d 634	. . . . . . 7 ⊢ (𝑦 = 𝑧 → ((𝜑 ∧ 𝑤 = 𝐵) ↔ (𝜒 ∧ 𝑤 = 𝐹)))
52	51	cbvrexvw 3359	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑤 = 𝐵) ↔ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹))
53	47, 52	bitrdi 290	. . . . 5 ⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)))
54	53	eu4 2616	. . . 4 ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∀𝑥∀𝑤((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)))
55	23, 44, 54	sylanbrc 586	. . 3 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))
56	18	iota2 6369	. . 3 ⊢ ((𝐶 ∈ V ∧ ∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) ↔ (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶))
57	15, 55, 56	syl2anc 587	. 2 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) ↔ (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶))
58	9, 57	mpbid 235	1 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541   = wceq 1543  ∃wex 1787   ∈ wcel 2110  ∃!weu 2567  ∀wral 3061  ∃wrex 3062  Vcvv 3408  ⦋csb 3811  ℩cio 6336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-nul 5199

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ral 3066  df-rex 3067  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-sn 4542  df-pr 4544  df-uni 4820  df-iota 6338

This theorem is referenced by: (None)