Theorem dfid3 5455

Description: A stronger version of df-id 5453 that does not require 𝑥 and 𝑦 to be disjoint. This is not the "official" definition since our definition soundness check without this requirement would be much more complex. The proof can be instructive in showing how disjoint variable requirements may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008.) (Revised by Mario Carneiro, 18-Nov-2016.) Use directly the definition df-id 5453 when sufficient, since the derivation of dfid3 5455 is nontrivial and uses auxiliary axioms ax-10 2139 to ax-13 2384. (New usage is discouraged.)

Assertion

Ref	Expression
dfid3	⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}

Proof of Theorem dfid3

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-id 5453	. 2 ⊢ I = {⟨𝑥, 𝑧⟩ ∣ 𝑥 = 𝑧}
2		equcom 2019	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥)
3	2	anbi1ci 627	. . . . . . . . . 10 ⊢ ((𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑧 = 𝑥 ∧ 𝑤 = ⟨𝑥, 𝑧⟩))
4	3	exbii 1842	. . . . . . . . 9 ⊢ (∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑤 = ⟨𝑥, 𝑧⟩))
5		opeq2 4796	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑥 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑥⟩)
6	5	eqeq2d 2830	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑤 = ⟨𝑥, 𝑧⟩ ↔ 𝑤 = ⟨𝑥, 𝑥⟩))
7	6	equsexvw 2005	. . . . . . . . 9 ⊢ (∃𝑧(𝑧 = 𝑥 ∧ 𝑤 = ⟨𝑥, 𝑧⟩) ↔ 𝑤 = ⟨𝑥, 𝑥⟩)
8		equid 2013	. . . . . . . . . 10 ⊢ 𝑥 = 𝑥
9	8	biantru 532	. . . . . . . . 9 ⊢ (𝑤 = ⟨𝑥, 𝑥⟩ ↔ (𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
10	4, 7, 9	3bitri 299	. . . . . . . 8 ⊢ (∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
11	10	exbii 1842	. . . . . . 7 ⊢ (∃𝑥∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
12		nfe1 2148	. . . . . . . 8 ⊢ Ⅎ𝑥∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥)
13	12	19.9 2198	. . . . . . 7 ⊢ (∃𝑥∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ ∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
14	11, 13	bitr4i 280	. . . . . 6 ⊢ (∃𝑥∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥))
15		opeq2 4796	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑥⟩ = ⟨𝑥, 𝑦⟩)
16	15	eqeq2d 2830	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑤 = ⟨𝑥, 𝑥⟩ ↔ 𝑤 = ⟨𝑥, 𝑦⟩))
17		equequ2 2027	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 ↔ 𝑥 = 𝑦))
18	16, 17	anbi12d 632	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
19	18	sps 2177	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
20	19	drex1 2457	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ ∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
21	20	drex2 2458	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑥(𝑤 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑥) ↔ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
22	14, 21	syl5bb 285	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
23		nfnae 2450	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
24		nfnae 2450	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑦
25		nfcvd 2976	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑤)
26		nfcvf2 3006	. . . . . . . . . 10 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥)
27		nfcvd 2976	. . . . . . . . . 10 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑧)
28	26, 27	nfopd 4812	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦⟨𝑥, 𝑧⟩)
29	25, 28	nfeqd 2986	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑤 = ⟨𝑥, 𝑧⟩)
30	26, 27	nfeqd 2986	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑧)
31	29, 30	nfand 1892	. . . . . . 7 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧))
32		opeq2 4796	. . . . . . . . . 10 ⊢ (𝑧 = 𝑦 → ⟨𝑥, 𝑧⟩ = ⟨𝑥, 𝑦⟩)
33	32	eqeq2d 2830	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑤 = ⟨𝑥, 𝑧⟩ ↔ 𝑤 = ⟨𝑥, 𝑦⟩))
34		equequ2 2027	. . . . . . . . 9 ⊢ (𝑧 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦))
35	33, 34	anbi12d 632	. . . . . . . 8 ⊢ (𝑧 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
36	35	a1i 11	. . . . . . 7 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ((𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ (𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦))))
37	24, 31, 36	cbvexd 2423	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
38	23, 37	exbid 2218	. . . . 5 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)))
39	22, 38	pm2.61i 184	. . . 4 ⊢ (∃𝑥∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦))
40	39	abbii 2884	. . 3 ⊢ {𝑤 ∣ ∃𝑥∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧)} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)}
41		df-opab 5120	. . 3 ⊢ {⟨𝑥, 𝑧⟩ ∣ 𝑥 = 𝑧} = {𝑤 ∣ ∃𝑥∃𝑧(𝑤 = ⟨𝑥, 𝑧⟩ ∧ 𝑥 = 𝑧)}
42		df-opab 5120	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)}
43	40, 41, 42	3eqtr4i 2852	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ 𝑥 = 𝑧} = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}
44	1, 43	eqtri 2842	1 ⊢ I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1529   = wceq 1531  ∃wex 1774  {cab 2797  ⟨cop 4565  {copab 5119   I cid 5452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-13 2384  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-opab 5120  df-id 5453

This theorem is referenced by:  dfid2  5456