Theorem dfid3 4796

Description: A stronger version of df-id 4795 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 4795	. 2 |- _I = { <. x , z >. | x = z }
2		ancom 450	. . . . . . . . . . 11 |- ( ( w = <. x , z >. /\ x = z ) <-> ( x = z /\ w = <. x , z >. ) )
3		equcom 1743	. . . . . . . . . . . 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 1644	. . . . . . . . 9 |- ( E. z ( w = <. x , z >. /\ x = z ) <-> E. z ( z = x /\ w = <. x , z >. ) )
7		vex 3116	. . . . . . . . . 10 |- x e. _V
8		opeq2 4214	. . . . . . . . . . 11 |- ( z = x -> <. x , z >. = <. x , x >. )
9	8	eqeq2d 2481	. . . . . . . . . 10 |- ( z = x -> ( w = <. x , z >. <-> w = <. x , x >. ) )
10	7, 9	ceqsexv 3150	. . . . . . . . 9 |- ( E. z ( z = x /\ w = <. x , z >. ) <-> w = <. x , x >. )
11		equid 1740	. . . . . . . . . 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 1644	. . . . . . 7 |- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x ( w = <. x , x >. /\ x = x ) )
15		nfe1 1789	. . . . . . . 8 |- F/ x E. x ( w = <. x , x >. /\ x = x )
16	15	19.9 1841	. . . . . . 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 4214	. . . . . . . . . . 11 |- ( x = y -> <. x , x >. = <. x , y >. )
19	18	eqeq2d 2481	. . . . . . . . . 10 |- ( x = y -> ( w = <. x , x >. <-> w = <. x , y >. ) )
20		equequ2 1748	. . . . . . . . . 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 1814	. . . . . . . 8 |- ( A. x x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) )
23	22	drex1 2042	. . . . . . 7 |- ( A. x x = y -> ( E. x ( w = <. x , x >. /\ x = x ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
24	23	drex2 2043	. . . . . 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 2031	. . . . . 6 |- F/ x -. A. x x = y
27		nfnae 2031	. . . . . . 7 |- F/ y -. A. x x = y
28		nfcvd 2630	. . . . . . . . 9 |- ( -. A. x x = y -> F/_ y w )
29		nfcvf2 2655	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ y x )
30		nfcvd 2630	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ y z )
31	29, 30	nfopd 4230	. . . . . . . . 9 |- ( -. A. x x = y -> F/_ y <. x , z >. )
32	28, 31	nfeqd 2636	. . . . . . . 8 |- ( -. A. x x = y -> F/ y w = <. x , z >. )
33	29, 30	nfeqd 2636	. . . . . . . 8 |- ( -. A. x x = y -> F/ y x = z )
34	32, 33	nfand 1872	. . . . . . 7 |- ( -. A. x x = y -> F/ y ( w = <. x , z >. /\ x = z ) )
35		opeq2 4214	. . . . . . . . . 10 |- ( z = y -> <. x , z >. = <. x , y >. )
36	35	eqeq2d 2481	. . . . . . . . 9 |- ( z = y -> ( w = <. x , z >. <-> w = <. x , y >. ) )
37		equequ2 1748	. . . . . . . . 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 1999	. . . . . 6 |- ( -. A. x x = y -> ( E. z ( w = <. x , z >. /\ x = z ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
41	26, 40	exbid 1834	. . . . 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 2601	. . 3 |- { w | E. x E. z ( w = <. x , z >. /\ x = z ) } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
44		df-opab 4506	. . 3 |- { <. x , z >. | x = z } = { w | E. x E. z ( w = <. x , z >. /\ x = z ) }
45		df-opab 4506	. . 3 |- { <. x , y >. | x = y } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
46	43, 44, 45	3eqtr4i 2506	. 2 |- { <. x , z >. | x = z } = { <. x , y >. | x = y }
47	1, 46	eqtri 2496	1 |- _I = { <. x , y >. | x = y }

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   A.wal 1377   = wceq 1379   E.wex 1596   {cab 2452   <.cop 4033   {copab 4504   _I cid 4790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-opab 4506  df-id 4795

This theorem is referenced by:  dfid2  4797  reli  5129  opabresid  5326  ider  7345  cnmptid  19913