Theorem unirep 35798

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 2739	. . . . 5 ⊢ (𝜓 → 𝐶 = 𝐶)
2	1	ancli 548	. . . 4 ⊢ (𝜓 → (𝜓 ∧ 𝐶 = 𝐶))
3		unirep.1	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝜑 ↔ 𝜓))
4		unirep.2	. . . . . . 7 ⊢ (𝑦 = 𝐷 → 𝐵 = 𝐶)
5	4	eqeq2d 2749	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝐶 = 𝐵 ↔ 𝐶 = 𝐶))
6	3, 5	anbi12d 630	. . . . 5 ⊢ (𝑦 = 𝐷 → ((𝜑 ∧ 𝐶 = 𝐵) ↔ (𝜓 ∧ 𝐶 = 𝐶)))
7	6	rspcev 3552	. . . 4 ⊢ ((𝐷 ∈ 𝐴 ∧ (𝜓 ∧ 𝐶 = 𝐶)) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
8	2, 7	sylan2 592	. . 3 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
9	8	adantl 481	. 2 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
10		nfcvd 2907	. . . . . 6 ⊢ (𝐷 ∈ 𝐴 → Ⅎ𝑦𝐶)
11	10, 4	csbiegf 3862	. . . . 5 ⊢ (𝐷 ∈ 𝐴 → ⦋𝐷 / 𝑦⦌𝐵 = 𝐶)
12		unirep.5	. . . . . 6 ⊢ 𝐵 ∈ V
13	12	csbex 5230	. . . . 5 ⊢ ⦋𝐷 / 𝑦⦌𝐵 ∈ V
14	11, 13	eqeltrrdi 2848	. . . 4 ⊢ (𝐷 ∈ 𝐴 → 𝐶 ∈ V)
15	14	ad2antrl 724	. . 3 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → 𝐶 ∈ V)
16		eqeq1 2742	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐶 → (𝑥 = 𝐵 ↔ 𝐶 = 𝐵))
17	16	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑥 = 𝐶 → ((𝜑 ∧ 𝑥 = 𝐵) ↔ (𝜑 ∧ 𝐶 = 𝐵)))
18	17	rexbidv 3225	. . . . . . . . 9 ⊢ (𝑥 = 𝐶 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵)))
19	18	spcegv 3526	. . . . . . . 8 ⊢ (𝐶 ∈ V → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)))
20	14, 19	syl 17	. . . . . . 7 ⊢ (𝐷 ∈ 𝐴 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)))
21	20	adantr 480	. . . . . 6 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)))
22	8, 21	mpd 15	. . . . 5 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))
23	22	adantl 481	. . . 4 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))
24		r19.29 3183	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → ∃𝑦 ∈ 𝐴 (∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)))
25		r19.29 3183	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → ∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)))
26		an4 652	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 = 𝐵) ∧ (𝜒 ∧ 𝑤 = 𝐹)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝑥 = 𝐵 ∧ 𝑤 = 𝐹)))
27		pm3.35 799	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹)) → 𝐵 = 𝐹)
28		eqeq12 2755	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → (𝑥 = 𝑤 ↔ 𝐵 = 𝐹))
29	27, 28	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹)) → ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
30	29	ancoms 458	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝜒)) → ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
31	30	expimpd 453	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜑 ∧ 𝜒) ∧ (𝑥 = 𝐵 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
32	26, 31	syl5bi 241	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜑 ∧ 𝑥 = 𝐵) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
33	32	ancomsd 465	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜒 ∧ 𝑤 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤))
34	33	expdimp 452	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝑤))
35	34	rexlimivw 3210	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝑤))
36	35	imp 406	. . . . . . . . . . . 12 ⊢ ((∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤)
37	25, 36	sylan 579	. . . . . . . . . . 11 ⊢ (((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤)
38	37	an32s 648	. . . . . . . . . 10 ⊢ (((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)
39	38	ex 412	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
40	39	rexlimivw 3210	. . . . . . . 8 ⊢ (∃𝑦 ∈ 𝐴 (∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
41	24, 40	syl 17	. . . . . . 7 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
42	41	expimpd 453	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → ((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
43	42	adantr 480	. . . . 5 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
44	43	alrimivv 1932	. . . 4 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∀𝑥∀𝑤((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
45		eqeq1 2742	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝐵 ↔ 𝑤 = 𝐵))
46	45	anbi2d 628	. . . . . . 7 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 = 𝐵) ↔ (𝜑 ∧ 𝑤 = 𝐵)))
47	46	rexbidv 3225	. . . . . 6 ⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑤 = 𝐵)))
48		unirep.3	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))
49		unirep.4	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → 𝐵 = 𝐹)
50	49	eqeq2d 2749	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝑤 = 𝐵 ↔ 𝑤 = 𝐹))
51	48, 50	anbi12d 630	. . . . . . 7 ⊢ (𝑦 = 𝑧 → ((𝜑 ∧ 𝑤 = 𝐵) ↔ (𝜒 ∧ 𝑤 = 𝐹)))
52	51	cbvrexvw 3373	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑤 = 𝐵) ↔ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹))
53	47, 52	bitrdi 286	. . . . 5 ⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)))
54	53	eu4 2617	. . . 4 ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∀𝑥∀𝑤((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)))
55	23, 44, 54	sylanbrc 582	. . 3 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))
56	18	iota2 6407	. . 3 ⊢ ((𝐶 ∈ V ∧ ∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) ↔ (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶))
57	15, 55, 56	syl2anc 583	. 2 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) ↔ (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶))
58	9, 57	mpbid 231	1 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ∃!weu 2568  ∀wral 3063  ∃wrex 3064  Vcvv 3422  ⦋csb 3828  ℩cio 6374

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  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-ral 3068  df-rex 3069  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559  df-pr 4561  df-uni 4837  df-iota 6376

This theorem is referenced by: (None)