Theorem dfid3 4805

Description: A stronger version of df-id 4804 that doesn't require x and y to be distinct. Ordinarily, we wouldn't use this as a definition, since non-distinct dummy variables would make soundness verification more difficult (as the proof here shows). The proof can be instructive in showing how distinct 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.)

Assertion

Ref	Expression
dfid3	|- _I = { <. x , y >. | x = y }

Proof of Theorem dfid3

Dummy variables z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-id 4804	. 2 |- _I = { <. x , z >. | x = z }
2		ancom 450	. . . . . . . . . . 11 |- ( ( w = <. x , z >. /\ x = z ) <-> ( x = z /\ w = <. x , z >. ) )
3		equcom 1795	. . . . . . . . . . . 12 |- ( x = z <-> z = x )
4	3	anbi1i 695	. . . . . . . . . . 11 |- ( ( x = z /\ w = <. x , z >. ) <-> ( z = x /\ w = <. x , z >. ) )
5	2, 4	bitri 249	. . . . . . . . . 10 |- ( ( w = <. x , z >. /\ x = z ) <-> ( z = x /\ w = <. x , z >. ) )
6	5	exbii 1668	. . . . . . . . 9 |- ( E. z ( w = <. x , z >. /\ x = z ) <-> E. z ( z = x /\ w = <. x , z >. ) )
7		vex 3112	. . . . . . . . . 10 |- x e. _V
8		opeq2 4220	. . . . . . . . . . 11 |- ( z = x -> <. x , z >. = <. x , x >. )
9	8	eqeq2d 2471	. . . . . . . . . 10 |- ( z = x -> ( w = <. x , z >. <-> w = <. x , x >. ) )
10	7, 9	ceqsexv 3146	. . . . . . . . 9 |- ( E. z ( z = x /\ w = <. x , z >. ) <-> w = <. x , x >. )
11		equid 1792	. . . . . . . . . 10 |- x = x
12	11	biantru 505	. . . . . . . . 9 |- ( w = <. x , x >. <-> ( w = <. x , x >. /\ x = x ) )
13	6, 10, 12	3bitri 271	. . . . . . . 8 |- ( E. z ( w = <. x , z >. /\ x = z ) <-> ( w = <. x , x >. /\ x = x ) )
14	13	exbii 1668	. . . . . . 7 |- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x ( w = <. x , x >. /\ x = x ) )
15		nfe1 1841	. . . . . . . 8 |- F/ x E. x ( w = <. x , x >. /\ x = x )
16	15	19.9 1894	. . . . . . 7 |- ( E. x E. x ( w = <. x , x >. /\ x = x ) <-> E. x ( w = <. x , x >. /\ x = x ) )
17	14, 16	bitr4i 252	. . . . . 6 |- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. x ( w = <. x , x >. /\ x = x ) )
18		opeq2 4220	. . . . . . . . . . 11 |- ( x = y -> <. x , x >. = <. x , y >. )
19	18	eqeq2d 2471	. . . . . . . . . 10 |- ( x = y -> ( w = <. x , x >. <-> w = <. x , y >. ) )
20		equequ2 1800	. . . . . . . . . 10 |- ( x = y -> ( x = x <-> x = y ) )
21	19, 20	anbi12d 710	. . . . . . . . 9 |- ( x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) )
22	21	sps 1866	. . . . . . . 8 |- ( A. x x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) )
23	22	drex1 2070	. . . . . . 7 |- ( A. x x = y -> ( E. x ( w = <. x , x >. /\ x = x ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
24	23	drex2 2071	. . . . . 6 |- ( A. x x = y -> ( E. x E. x ( w = <. x , x >. /\ x = x ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) ) )
25	17, 24	syl5bb 257	. . . . 5 |- ( A. x x = y -> ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) ) )
26		nfnae 2059	. . . . . 6 |- F/ x -. A. x x = y
27		nfnae 2059	. . . . . . 7 |- F/ y -. A. x x = y
28		nfcvd 2620	. . . . . . . . 9 |- ( -. A. x x = y -> F/_ y w )
29		nfcvf2 2645	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ y x )
30		nfcvd 2620	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ y z )
31	29, 30	nfopd 4236	. . . . . . . . 9 |- ( -. A. x x = y -> F/_ y <. x , z >. )
32	28, 31	nfeqd 2626	. . . . . . . 8 |- ( -. A. x x = y -> F/ y w = <. x , z >. )
33	29, 30	nfeqd 2626	. . . . . . . 8 |- ( -. A. x x = y -> F/ y x = z )
34	32, 33	nfand 1926	. . . . . . 7 |- ( -. A. x x = y -> F/ y ( w = <. x , z >. /\ x = z ) )
35		opeq2 4220	. . . . . . . . . 10 |- ( z = y -> <. x , z >. = <. x , y >. )
36	35	eqeq2d 2471	. . . . . . . . 9 |- ( z = y -> ( w = <. x , z >. <-> w = <. x , y >. ) )
37		equequ2 1800	. . . . . . . . 9 |- ( z = y -> ( x = z <-> x = y ) )
38	36, 37	anbi12d 710	. . . . . . . 8 |- ( z = y -> ( ( w = <. x , z >. /\ x = z ) <-> ( w = <. x , y >. /\ x = y ) ) )
39	38	a1i 11	. . . . . . 7 |- ( -. A. x x = y -> ( z = y -> ( ( w = <. x , z >. /\ x = z ) <-> ( w = <. x , y >. /\ x = y ) ) ) )
40	27, 34, 39	cbvexd 2027	. . . . . 6 |- ( -. A. x x = y -> ( E. z ( w = <. x , z >. /\ x = z ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
41	26, 40	exbid 1887	. . . . 5 |- ( -. A. x x = y -> ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) ) )
42	25, 41	pm2.61i 164	. . . 4 |- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) )
43	42	abbii 2591	. . 3 |- { w | E. x E. z ( w = <. x , z >. /\ x = z ) } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
44		df-opab 4516	. . 3 |- { <. x , z >. | x = z } = { w | E. x E. z ( w = <. x , z >. /\ x = z ) }
45		df-opab 4516	. . 3 |- { <. x , y >. | x = y } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
46	43, 44, 45	3eqtr4i 2496	. 2 |- { <. x , z >. | x = z } = { <. x , y >. | x = y }
47	1, 46	eqtri 2486	1 |- _I = { <. x , y >. | x = y }

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1393   = wceq 1395   E.wex 1613   {cab 2442   <.cop 4038   {copab 4514   _I cid 4799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-opab 4516  df-id 4804

This theorem is referenced by:  dfid2  4806  reli  5140  opabresid  5337  ider  7363  cnmptid  20287