Theorem unirep 33507

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 2623	. . . . 5 ⊢ (𝜓 → 𝐶 = 𝐶)
2	1	ancli 574	. . . 4 ⊢ (𝜓 → (𝜓 ∧ 𝐶 = 𝐶))
3		unirep.1	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝜑 ↔ 𝜓))
4		unirep.2	. . . . . . 7 ⊢ (𝑦 = 𝐷 → 𝐵 = 𝐶)
5	4	eqeq2d 2632	. . . . . 6 ⊢ (𝑦 = 𝐷 → (𝐶 = 𝐵 ↔ 𝐶 = 𝐶))
6	3, 5	anbi12d 747	. . . . 5 ⊢ (𝑦 = 𝐷 → ((𝜑 ∧ 𝐶 = 𝐵) ↔ (𝜓 ∧ 𝐶 = 𝐶)))
7	6	rspcev 3309	. . . 4 ⊢ ((𝐷 ∈ 𝐴 ∧ (𝜓 ∧ 𝐶 = 𝐶)) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
8	2, 7	sylan2 491	. . 3 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
9	8	adantl 482	. 2 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵))
10		nfcvd 2765	. . . . . 6 ⊢ (𝐷 ∈ 𝐴 → Ⅎ𝑦𝐶)
11	10, 4	csbiegf 3557	. . . . 5 ⊢ (𝐷 ∈ 𝐴 → ⦋𝐷 / 𝑦⦌𝐵 = 𝐶)
12		unirep.5	. . . . . 6 ⊢ 𝐵 ∈ V
13	12	csbex 4793	. . . . 5 ⊢ ⦋𝐷 / 𝑦⦌𝐵 ∈ V
14	11, 13	syl6eqelr 2710	. . . 4 ⊢ (𝐷 ∈ 𝐴 → 𝐶 ∈ V)
15	14	ad2antrl 764	. . 3 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → 𝐶 ∈ V)
16		eqeq1 2626	. . . . . . . . . . 11 ⊢ (𝑥 = 𝐶 → (𝑥 = 𝐵 ↔ 𝐶 = 𝐵))
17	16	anbi2d 740	. . . . . . . . . 10 ⊢ (𝑥 = 𝐶 → ((𝜑 ∧ 𝑥 = 𝐵) ↔ (𝜑 ∧ 𝐶 = 𝐵)))
18	17	rexbidv 3052	. . . . . . . . 9 ⊢ (𝑥 = 𝐶 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵)))
19	18	spcegv 3294	. . . . . . . 8 ⊢ (𝐶 ∈ V → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)))
20	14, 19	syl 17	. . . . . . 7 ⊢ (𝐷 ∈ 𝐴 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)))
21	20	adantr 481	. . . . . 6 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)))
22	8, 21	mpd 15	. . . . 5 ⊢ ((𝐷 ∈ 𝐴 ∧ 𝜓) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))
23	22	adantl 482	. . . 4 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))
24		r19.29 3072	. . . . . . . 8 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → ∃𝑦 ∈ 𝐴 (∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)))
25		r19.29 3072	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → ∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)))
26		an4 865	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 = 𝐵) ∧ (𝜒 ∧ 𝑤 = 𝐹)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝑥 = 𝐵 ∧ 𝑤 = 𝐹)))
27		pm3.35 611	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹)) → 𝐵 = 𝐹)
28		eqeq12 2635	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → (𝑥 = 𝑤 ↔ 𝐵 = 𝐹))
29	27, 28	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝜒) ∧ ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹)) → ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
30	29	ancoms 469	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝜒)) → ((𝑥 = 𝐵 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
31	30	expimpd 629	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜑 ∧ 𝜒) ∧ (𝑥 = 𝐵 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
32	26, 31	syl5bi 232	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜑 ∧ 𝑥 = 𝐵) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
33	32	ancomsd 470	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → (((𝜒 ∧ 𝑤 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤))
34	33	expdimp 453	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝑤))
35	34	rexlimivw 3029	. . . . . . . . . . . . 13 ⊢ (∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) → ((𝜑 ∧ 𝑥 = 𝐵) → 𝑥 = 𝑤))
36	35	imp 445	. . . . . . . . . . . 12 ⊢ ((∃𝑧 ∈ 𝐴 (((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜒 ∧ 𝑤 = 𝐹)) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤)
37	25, 36	sylan 488	. . . . . . . . . . 11 ⊢ (((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → 𝑥 = 𝑤)
38	37	an32s 846	. . . . . . . . . 10 ⊢ (((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)
39	38	ex 450	. . . . . . . . 9 ⊢ ((∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
40	39	rexlimivw 3029	. . . . . . . 8 ⊢ (∃𝑦 ∈ 𝐴 (∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
41	24, 40	syl 17	. . . . . . 7 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹) → 𝑥 = 𝑤))
42	41	expimpd 629	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) → ((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
43	42	adantr 481	. . . . 5 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
44	43	alrimivv 1856	. . . 4 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∀𝑥∀𝑤((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤))
45		eqeq1 2626	. . . . . . . 8 ⊢ (𝑥 = 𝑤 → (𝑥 = 𝐵 ↔ 𝑤 = 𝐵))
46	45	anbi2d 740	. . . . . . 7 ⊢ (𝑥 = 𝑤 → ((𝜑 ∧ 𝑥 = 𝐵) ↔ (𝜑 ∧ 𝑤 = 𝐵)))
47	46	rexbidv 3052	. . . . . 6 ⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑤 = 𝐵)))
48		unirep.3	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜒))
49		unirep.4	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → 𝐵 = 𝐹)
50	49	eqeq2d 2632	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (𝑤 = 𝐵 ↔ 𝑤 = 𝐹))
51	48, 50	anbi12d 747	. . . . . . 7 ⊢ (𝑦 = 𝑧 → ((𝜑 ∧ 𝑤 = 𝐵) ↔ (𝜒 ∧ 𝑤 = 𝐹)))
52	51	cbvrexv 3172	. . . . . 6 ⊢ (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑤 = 𝐵) ↔ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹))
53	47, 52	syl6bb 276	. . . . 5 ⊢ (𝑥 = 𝑤 → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)))
54	53	eu4 2518	. . . 4 ⊢ (∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ↔ (∃𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∀𝑥∀𝑤((∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵) ∧ ∃𝑧 ∈ 𝐴 (𝜒 ∧ 𝑤 = 𝐹)) → 𝑥 = 𝑤)))
55	23, 44, 54	sylanbrc 698	. . 3 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → ∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵))
56	18	iota2 5877	. . 3 ⊢ ((𝐶 ∈ V ∧ ∃!𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) ↔ (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶))
57	15, 55, 56	syl2anc 693	. 2 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝐶 = 𝐵) ↔ (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶))
58	9, 57	mpbid 222	1 ⊢ ((∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝜑 ∧ 𝜒) → 𝐵 = 𝐹) ∧ (𝐷 ∈ 𝐴 ∧ 𝜓)) → (℩𝑥∃𝑦 ∈ 𝐴 (𝜑 ∧ 𝑥 = 𝐵)) = 𝐶)

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1481   = wceq 1483  ∃wex 1704   ∈ wcel 1990  ∃!weu 2470  ∀wral 2912  ∃wrex 2913  Vcvv 3200  ⦋csb 3533  ℩cio 5849

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437  df-iota 5851

This theorem is referenced by: (None)