Theorem dfid3 4769

Description: A stronger version of df-id 4768 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 4768	. 2 |- _I = { <. x , z >. | x = z }
2		ancom 456	. . . . . . . . . . 11 |- ( ( w = <. x , z >. /\ x = z ) <-> ( x = z /\ w = <. x , z >. ) )
3		equcom 1873	. . . . . . . . . . . 12 |- ( x = z <-> z = x )
4	3	anbi1i 706	. . . . . . . . . . 11 |- ( ( x = z /\ w = <. x , z >. ) <-> ( z = x /\ w = <. x , z >. ) )
5	2, 4	bitri 257	. . . . . . . . . 10 |- ( ( w = <. x , z >. /\ x = z ) <-> ( z = x /\ w = <. x , z >. ) )
6	5	exbii 1729	. . . . . . . . 9 |- ( E. z ( w = <. x , z >. /\ x = z ) <-> E. z ( z = x /\ w = <. x , z >. ) )
7		vex 3060	. . . . . . . . . 10 |- x e. _V
8		opeq2 4181	. . . . . . . . . . 11 |- ( z = x -> <. x , z >. = <. x , x >. )
9	8	eqeq2d 2472	. . . . . . . . . 10 |- ( z = x -> ( w = <. x , z >. <-> w = <. x , x >. ) )
10	7, 9	ceqsexv 3096	. . . . . . . . 9 |- ( E. z ( z = x /\ w = <. x , z >. ) <-> w = <. x , x >. )
11		equid 1866	. . . . . . . . . 10 |- x = x
12	11	biantru 512	. . . . . . . . 9 |- ( w = <. x , x >. <-> ( w = <. x , x >. /\ x = x ) )
13	6, 10, 12	3bitri 279	. . . . . . . 8 |- ( E. z ( w = <. x , z >. /\ x = z ) <-> ( w = <. x , x >. /\ x = x ) )
14	13	exbii 1729	. . . . . . 7 |- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x ( w = <. x , x >. /\ x = x ) )
15		nfe1 1929	. . . . . . . 8 |- F/ x E. x ( w = <. x , x >. /\ x = x )
16	15	19.9 1981	. . . . . . 7 |- ( E. x E. x ( w = <. x , x >. /\ x = x ) <-> E. x ( w = <. x , x >. /\ x = x ) )
17	14, 16	bitr4i 260	. . . . . 6 |- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. x ( w = <. x , x >. /\ x = x ) )
18		opeq2 4181	. . . . . . . . . . 11 |- ( x = y -> <. x , x >. = <. x , y >. )
19	18	eqeq2d 2472	. . . . . . . . . 10 |- ( x = y -> ( w = <. x , x >. <-> w = <. x , y >. ) )
20		equequ2 1879	. . . . . . . . . 10 |- ( x = y -> ( x = x <-> x = y ) )
21	19, 20	anbi12d 722	. . . . . . . . 9 |- ( x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) )
22	21	sps 1954	. . . . . . . 8 |- ( A. x x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) )
23	22	drex1 2172	. . . . . . 7 |- ( A. x x = y -> ( E. x ( w = <. x , x >. /\ x = x ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
24	23	drex2 2173	. . . . . 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 265	. . . . 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 2163	. . . . . 6 |- F/ x -. A. x x = y
27		nfnae 2163	. . . . . . 7 |- F/ y -. A. x x = y
28		nfcvd 2604	. . . . . . . . 9 |- ( -. A. x x = y -> F/_ y w )
29		nfcvf2 2627	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ y x )
30		nfcvd 2604	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ y z )
31	29, 30	nfopd 4197	. . . . . . . . 9 |- ( -. A. x x = y -> F/_ y <. x , z >. )
32	28, 31	nfeqd 2610	. . . . . . . 8 |- ( -. A. x x = y -> F/ y w = <. x , z >. )
33	29, 30	nfeqd 2610	. . . . . . . 8 |- ( -. A. x x = y -> F/ y x = z )
34	32, 33	nfand 2019	. . . . . . 7 |- ( -. A. x x = y -> F/ y ( w = <. x , z >. /\ x = z ) )
35		opeq2 4181	. . . . . . . . . 10 |- ( z = y -> <. x , z >. = <. x , y >. )
36	35	eqeq2d 2472	. . . . . . . . 9 |- ( z = y -> ( w = <. x , z >. <-> w = <. x , y >. ) )
37		equequ2 1879	. . . . . . . . 9 |- ( z = y -> ( x = z <-> x = y ) )
38	36, 37	anbi12d 722	. . . . . . . 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 2130	. . . . . 6 |- ( -. A. x x = y -> ( E. z ( w = <. x , z >. /\ x = z ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
41	26, 40	exbid 1975	. . . . 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 169	. . . 4 |- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) )
43	42	abbii 2578	. . 3 |- { w | E. x E. z ( w = <. x , z >. /\ x = z ) } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
44		df-opab 4476	. . 3 |- { <. x , z >. | x = z } = { w | E. x E. z ( w = <. x , z >. /\ x = z ) }
45		df-opab 4476	. . 3 |- { <. x , y >. | x = y } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
46	43, 44, 45	3eqtr4i 2494	. 2 |- { <. x , z >. | x = z } = { <. x , y >. | x = y }
47	1, 46	eqtri 2484	1 |- _I = { <. x , y >. | x = y }

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 375   A.wal 1453   = wceq 1455   E.wex 1674   {cab 2448   <.cop 3986   {copab 4474   _I cid 4763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-opab 4476  df-id 4768

This theorem is referenced by:  dfid2  4771  reli  4981  opabresid  5177  ider  7423  cnmptid  20725