Theorem dfid3 4770

Description: A stronger version of df-id 4769 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 4769	. 2 |- _I = { <. x , z >. | x = z }
2		ancom 451	. . . . . . . . . . 11 |- ( ( w = <. x , z >. /\ x = z ) <-> ( x = z /\ w = <. x , z >. ) )
3		equcom 1846	. . . . . . . . . . . 12 |- ( x = z <-> z = x )
4	3	anbi1i 699	. . . . . . . . . . 11 |- ( ( x = z /\ w = <. x , z >. ) <-> ( z = x /\ w = <. x , z >. ) )
5	2, 4	bitri 252	. . . . . . . . . 10 |- ( ( w = <. x , z >. /\ x = z ) <-> ( z = x /\ w = <. x , z >. ) )
6	5	exbii 1714	. . . . . . . . 9 |- ( E. z ( w = <. x , z >. /\ x = z ) <-> E. z ( z = x /\ w = <. x , z >. ) )
7		vex 3090	. . . . . . . . . 10 |- x e. _V
8		opeq2 4191	. . . . . . . . . . 11 |- ( z = x -> <. x , z >. = <. x , x >. )
9	8	eqeq2d 2443	. . . . . . . . . 10 |- ( z = x -> ( w = <. x , z >. <-> w = <. x , x >. ) )
10	7, 9	ceqsexv 3124	. . . . . . . . 9 |- ( E. z ( z = x /\ w = <. x , z >. ) <-> w = <. x , x >. )
11		equid 1842	. . . . . . . . . 10 |- x = x
12	11	biantru 507	. . . . . . . . 9 |- ( w = <. x , x >. <-> ( w = <. x , x >. /\ x = x ) )
13	6, 10, 12	3bitri 274	. . . . . . . 8 |- ( E. z ( w = <. x , z >. /\ x = z ) <-> ( w = <. x , x >. /\ x = x ) )
14	13	exbii 1714	. . . . . . 7 |- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x ( w = <. x , x >. /\ x = x ) )
15		nfe1 1892	. . . . . . . 8 |- F/ x E. x ( w = <. x , x >. /\ x = x )
16	15	19.9 1945	. . . . . . 7 |- ( E. x E. x ( w = <. x , x >. /\ x = x ) <-> E. x ( w = <. x , x >. /\ x = x ) )
17	14, 16	bitr4i 255	. . . . . 6 |- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. x ( w = <. x , x >. /\ x = x ) )
18		opeq2 4191	. . . . . . . . . . 11 |- ( x = y -> <. x , x >. = <. x , y >. )
19	18	eqeq2d 2443	. . . . . . . . . 10 |- ( x = y -> ( w = <. x , x >. <-> w = <. x , y >. ) )
20		equequ2 1851	. . . . . . . . . 10 |- ( x = y -> ( x = x <-> x = y ) )
21	19, 20	anbi12d 715	. . . . . . . . 9 |- ( x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) )
22	21	sps 1918	. . . . . . . 8 |- ( A. x x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) )
23	22	drex1 2125	. . . . . . 7 |- ( A. x x = y -> ( E. x ( w = <. x , x >. /\ x = x ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
24	23	drex2 2126	. . . . . 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 260	. . . . 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 2114	. . . . . 6 |- F/ x -. A. x x = y
27		nfnae 2114	. . . . . . 7 |- F/ y -. A. x x = y
28		nfcvd 2592	. . . . . . . . 9 |- ( -. A. x x = y -> F/_ y w )
29		nfcvf2 2617	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ y x )
30		nfcvd 2592	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ y z )
31	29, 30	nfopd 4207	. . . . . . . . 9 |- ( -. A. x x = y -> F/_ y <. x , z >. )
32	28, 31	nfeqd 2598	. . . . . . . 8 |- ( -. A. x x = y -> F/ y w = <. x , z >. )
33	29, 30	nfeqd 2598	. . . . . . . 8 |- ( -. A. x x = y -> F/ y x = z )
34	32, 33	nfand 1983	. . . . . . 7 |- ( -. A. x x = y -> F/ y ( w = <. x , z >. /\ x = z ) )
35		opeq2 4191	. . . . . . . . . 10 |- ( z = y -> <. x , z >. = <. x , y >. )
36	35	eqeq2d 2443	. . . . . . . . 9 |- ( z = y -> ( w = <. x , z >. <-> w = <. x , y >. ) )
37		equequ2 1851	. . . . . . . . 9 |- ( z = y -> ( x = z <-> x = y ) )
38	36, 37	anbi12d 715	. . . . . . . 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 2082	. . . . . 6 |- ( -. A. x x = y -> ( E. z ( w = <. x , z >. /\ x = z ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
41	26, 40	exbid 1939	. . . . 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 167	. . . 4 |- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) )
43	42	abbii 2563	. . 3 |- { w | E. x E. z ( w = <. x , z >. /\ x = z ) } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
44		df-opab 4485	. . 3 |- { <. x , z >. | x = z } = { w | E. x E. z ( w = <. x , z >. /\ x = z ) }
45		df-opab 4485	. . 3 |- { <. x , y >. | x = y } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
46	43, 44, 45	3eqtr4i 2468	. 2 |- { <. x , z >. | x = z } = { <. x , y >. | x = y }
47	1, 46	eqtri 2458	1 |- _I = { <. x , y >. | x = y }

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   A.wal 1435   = wceq 1437   E.wex 1659   {cab 2414   <.cop 4008   {copab 4483   _I cid 4764

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-opab 4485  df-id 4769

This theorem is referenced by:  dfid2  4772  reli  4982  opabresid  5178  ider  7405  cnmptid  20607