Theorem dfid3

Description: A stronger version of df-id that does not require x and y 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 when sufficient, since the derivation of dfid3 is nontrivial and uses auxiliary axioms ax-10 to ax-13 . (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-id	⊢ I = { ⟨ 𝑥 , 𝑧 ⟩ ∣ 𝑥 = 𝑧 }
2		equcom	⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 )
3	2	anbi1ci	⊢ ( ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ( 𝑧 = 𝑥 ∧ 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ) )
4	3	exbii	⊢ ( ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ) )
5		opeq2	⊢ ( 𝑧 = 𝑥 → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑥 ⟩ )
6	5	eqeq2d	⊢ ( 𝑧 = 𝑥 → ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ↔ 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ) )
7	6	equsexvw	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ) ↔ 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ )
8		equid	⊢ 𝑥 = 𝑥
9	8	biantru	⊢ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ↔ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) )
10	4 7 9	3bitri	⊢ ( ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) )
11	10	exbii	⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) )
12		nfe1	⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 )
13	12	19.9	⊢ ( ∃ 𝑥 ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) )
14	11 13	bitr4i	⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) )
15		opeq2	⊢ ( 𝑥 = 𝑦 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
16	15	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ↔ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
17		equequ2	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑥 ↔ 𝑥 = 𝑦 ) )
18	16 17	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) )
19	18	sps	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) )
20	19	drex1	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) )
21	20	drex2	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑥 ( 𝑤 = ⟨ 𝑥 , 𝑥 ⟩ ∧ 𝑥 = 𝑥 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) )
22	14 21	syl5bb	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) )
23		nfnae	⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦
24		nfnae	⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦
25		nfcvd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 )
26		nfcvf2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 )
27		nfcvd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑧 )
28	26 27	nfopd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ⟨ 𝑥 , 𝑧 ⟩ )
29	25 28	nfeqd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ )
30	26 27	nfeqd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 = 𝑧 )
31	29 30	nfand	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) )
32		opeq2	⊢ ( 𝑧 = 𝑦 → ⟨ 𝑥 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
33	32	eqeq2d	⊢ ( 𝑧 = 𝑦 → ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ↔ 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ) )
34		equequ2	⊢ ( 𝑧 = 𝑦 → ( 𝑥 = 𝑧 ↔ 𝑥 = 𝑦 ) )
35	33 34	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) )
36	35	a1i	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ( ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) ) )
37	24 31 36	cbvexd	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) )
38	23 37	exbid	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) ) )
39	22 38	pm2.61i	⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) )
40	39	abbii	⊢ { 𝑤 ∣ ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) }
41		df-opab	⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ 𝑥 = 𝑧 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑧 ( 𝑤 = ⟨ 𝑥 , 𝑧 ⟩ ∧ 𝑥 = 𝑧 ) }
42		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑤 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝑥 = 𝑦 ) }
43	40 41 42	3eqtr4i	⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ 𝑥 = 𝑧 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }
44	1 43	eqtri	⊢ I = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 = 𝑦 }