Theorem unirep 32677

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 2611	. . . . 5 ⊢ (𝜓 → 𝐶 = 𝐶)
2	1	ancli 572	. . . 4 ⊢ (𝜓 → (𝜓 ∧ 𝐶 = 𝐶))
3		unirep.1	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝜑 ↔ 𝜓))
4		unirep.2	. . . . . . 7 ⊢ (𝑦 = 𝐷 → 𝐵 = 𝐶)
5	4	eqeq2d 2620	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝐶 = 𝐵 ↔ 𝐶 = 𝐶))
6	3, 5	anbi12d 743	. . . . 5 ⊢ (𝑦 = 𝐷 → ((𝜑 ∧ 𝐶 = 𝐵) ↔ (𝜓 ∧ 𝐶 = 𝐶)))
7	6	rspcev 3282	. . . 4 ⊢ ((𝐷 ∈ 𝐴 ∧ (𝜓 ∧ 𝐶 = 𝐶)) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
8	2, 7	sylan2 490	. . 3 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
9	8	adantl 481	. 2 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
10		nfcvd 2752	. . . . . 6 ⊢ (𝐷 ∈ 𝐴 → Ⅎ𝑦𝐶)
11	10, 4	csbiegf 3523	. . . . 5 ⊢ (𝐷 ∈ 𝐴 → ⦋𝐷 / 𝑦⦌𝐵 = 𝐶)
12		unirep.5	. . . . . 6 ⊢ 𝐵 ∈ V
13	12	csbex 4721	. . . . 5 ⊢ ⦋𝐷 / 𝑦⦌𝐵 ∈ V
14	11, 13	syl6eqelr 2697	. . . 4 ⊢ (𝐷 ∈ 𝐴 → 𝐶 ∈ V)
15	14	ad2antrl 760	. . 3 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → 𝐶 ∈ V)
16		eqeq1 2614	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐶 → (𝑥 = 𝐵 ↔ 𝐶 = 𝐵))
17	16	anbi2d 736	. . . . . . . . . 10 ⊢ (𝑥 = 𝐶 → ((𝜑 ∧ 𝑥 = 𝐵) ↔ (𝜑 ∧ 𝐶 = 𝐵)))
18	17	rexbidv 3034	. . . . . . . . 9 ⊢ (𝑥 = 𝐶 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵)))
19	18	spcegv 3267	. . . . . . . 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 3054	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → ∃𝑦 ∈ 𝐴 (∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)))
25		r19.29 3054	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → ∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)))
26		an4 861	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 = 𝐵) ∧ (𝜒 ∧ 𝑤 = 𝐹)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝑥 = 𝐵 ∧ 𝑤 = 𝐹)))
27		pm3.35 609	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹)) → 𝐵 = 𝐹)
28		eqeq12 2623	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → (𝑥 = 𝑤 ↔ 𝐵 = 𝐹))
29	27, 28	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹)) → ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
30	29	ancoms 468	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝜒)) → ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
31	30	expimpd 627	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜑 ∧ 𝜒) ∧ (𝑥 = 𝐵 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
32	26, 31	syl5bi 231	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜑 ∧ 𝑥 = 𝐵) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
33	32	ancomsd 469	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜒 ∧ 𝑤 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤))
34	33	expdimp 452	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝑤))
35	34	rexlimivw 3011	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝑤))
36	35	imp 444	. . . . . . . . . . . 12 ⊢ ((∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤)
37	25, 36	sylan 487	. . . . . . . . . . 11 ⊢ (((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤)
38	37	an32s 842	. . . . . . . . . 10 ⊢ (((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)
39	38	ex 449	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
40	39	rexlimivw 3011	. . . . . . . 8 ⊢ (∃𝑦 ∈ 𝐴 (∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
41	24, 40	syl 17	. . . . . . 7 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
42	41	expimpd 627	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → ((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
43	42	adantr 480	. . . . 5 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
44	43	alrimivv 1843	. . . 4 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∀𝑥∀𝑤((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
45		eqeq1 2614	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝐵 ↔ 𝑤 = 𝐵))
46	45	anbi2d 736	. . . . . . 7 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 = 𝐵) ↔ (𝜑 ∧ 𝑤 = 𝐵)))
47	46	rexbidv 3034	. . . . . 6 ⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑤 = 𝐵)))
48		unirep.3	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))
49		unirep.4	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → 𝐵 = 𝐹)
50	49	eqeq2d 2620	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝑤 = 𝐵 ↔ 𝑤 = 𝐹))
51	48, 50	anbi12d 743	. . . . . . 7 ⊢ (𝑦 = 𝑧 → ((𝜑 ∧ 𝑤 = 𝐵) ↔ (𝜒 ∧ 𝑤 = 𝐹)))
52	51	cbvrexv 3148	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑤 = 𝐵) ↔ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹))
53	47, 52	syl6bb 275	. . . . 5 ⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)))
54	53	eu4 2506	. . . 4 ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∀𝑥∀𝑤((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)))
55	23, 44, 54	sylanbrc 695	. . 3 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))
56	18	iota2 5794	. . 3 ⊢ ((𝐶 ∈ V ∧ ∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) ↔ (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶))
57	15, 55, 56	syl2anc 691	. 2 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) ↔ (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶))
58	9, 57	mpbid 221	1 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶)

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃!weu 2458  ∀wral 2896  ∃wrex 2897  Vcvv 3173  ⦋csb 3499  ℩cio 5766

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-nul 3875  df-sn 4126  df-pr 4128  df-uni 4373  df-iota 5768

This theorem is referenced by: (None)