Theorem dfid3 4707

Description: A stronger version of df-id 4706 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 4706	. 2 |- _I = { <. x , z >. | x = z }
2		ancom 451	. . . . . . . . . . 11 |- ( ( w = <. x , z >. /\ x = z ) <-> ( x = z /\ w = <. x , z >. ) )
3		equcom 1848	. . . . . . . . . . . 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 1712	. . . . . . . . 9 |- ( E. z ( w = <. x , z >. /\ x = z ) <-> E. z ( z = x /\ w = <. x , z >. ) )
7		vex 3020	. . . . . . . . . 10 |- x e. _V
8		opeq2 4126	. . . . . . . . . . 11 |- ( z = x -> <. x , z >. = <. x , x >. )
9	8	eqeq2d 2433	. . . . . . . . . 10 |- ( z = x -> ( w = <. x , z >. <-> w = <. x , x >. ) )
10	7, 9	ceqsexv 3055	. . . . . . . . 9 |- ( E. z ( z = x /\ w = <. x , z >. ) <-> w = <. x , x >. )
11		equid 1844	. . . . . . . . . 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 1712	. . . . . . 7 |- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x ( w = <. x , x >. /\ x = x ) )
15		nfe1 1894	. . . . . . . 8 |- F/ x E. x ( w = <. x , x >. /\ x = x )
16	15	19.9 1947	. . . . . . 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 4126	. . . . . . . . . . 11 |- ( x = y -> <. x , x >. = <. x , y >. )
19	18	eqeq2d 2433	. . . . . . . . . 10 |- ( x = y -> ( w = <. x , x >. <-> w = <. x , y >. ) )
20		equequ2 1853	. . . . . . . . . 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 1920	. . . . . . . 8 |- ( A. x x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) )
23	22	drex1 2130	. . . . . . 7 |- ( A. x x = y -> ( E. x ( w = <. x , x >. /\ x = x ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
24	23	drex2 2131	. . . . . 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 2119	. . . . . 6 |- F/ x -. A. x x = y
27		nfnae 2119	. . . . . . 7 |- F/ y -. A. x x = y
28		nfcvd 2565	. . . . . . . . 9 |- ( -. A. x x = y -> F/_ y w )
29		nfcvf2 2588	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ y x )
30		nfcvd 2565	. . . . . . . . . 10 |- ( -. A. x x = y -> F/_ y z )
31	29, 30	nfopd 4142	. . . . . . . . 9 |- ( -. A. x x = y -> F/_ y <. x , z >. )
32	28, 31	nfeqd 2571	. . . . . . . 8 |- ( -. A. x x = y -> F/ y w = <. x , z >. )
33	29, 30	nfeqd 2571	. . . . . . . 8 |- ( -. A. x x = y -> F/ y x = z )
34	32, 33	nfand 1985	. . . . . . 7 |- ( -. A. x x = y -> F/ y ( w = <. x , z >. /\ x = z ) )
35		opeq2 4126	. . . . . . . . . 10 |- ( z = y -> <. x , z >. = <. x , y >. )
36	35	eqeq2d 2433	. . . . . . . . 9 |- ( z = y -> ( w = <. x , z >. <-> w = <. x , y >. ) )
37		equequ2 1853	. . . . . . . . 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 2086	. . . . . 6 |- ( -. A. x x = y -> ( E. z ( w = <. x , z >. /\ x = z ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
41	26, 40	exbid 1941	. . . . 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 2539	. . 3 |- { w | E. x E. z ( w = <. x , z >. /\ x = z ) } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
44		df-opab 4421	. . 3 |- { <. x , z >. | x = z } = { w | E. x E. z ( w = <. x , z >. /\ x = z ) }
45		df-opab 4421	. . 3 |- { <. x , y >. | x = y } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
46	43, 44, 45	3eqtr4i 2455	. 2 |- { <. x , z >. | x = z } = { <. x , y >. | x = y }
47	1, 46	eqtri 2445	1 |- _I = { <. x , y >. | x = y }

Syntax hints:   -. wn 3   -> wi 4   <-> wb 187   /\ wa 370   A.wal 1435   = wceq 1437   E.wex 1657   {cab 2409   <.cop 3942   {copab 4419   _I cid 4701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-rab 2718  df-v 3019  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-sn 3937  df-pr 3939  df-op 3943  df-opab 4421  df-id 4706

This theorem is referenced by:  dfid2  4709  reli  4919  opabresid  5115  ider  7347  cnmptid  20613