Theorem dfid3

Description: A stronger version of df-id that does not require x and y to be disjoint. This is not the definition since, in order to pass our definition soundness test, a definition has to have disjoint dummy variables, see conventions . The proof can be instructive in showing how disjoint variable conditions may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008) (Revised by Mario Carneiro, 18-Nov-2016)

Use df-id instead to make the semantics of the constructor df-opab clearer (in usages, x , y will typically be dummy variables, so can be assumed disjoint). (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		df-id	|- _I = { <. x , z >. | x = z }
2		equcom	|- ( x = z <-> z = x )
3	2	anbi1ci	|- ( ( w = <. x , z >. /\ x = z ) <-> ( z = x /\ w = <. x , z >. ) )
4	3	exbii	|- ( E. z ( w = <. x , z >. /\ x = z ) <-> E. z ( z = x /\ w = <. x , z >. ) )
5		opeq2	|- ( z = x -> <. x , z >. = <. x , x >. )
6	5	eqeq2d	|- ( z = x -> ( w = <. x , z >. <-> w = <. x , x >. ) )
7	6	equsexvw	|- ( E. z ( z = x /\ w = <. x , z >. ) <-> w = <. x , x >. )
8		equid	|- x = x
9	8	biantru	|- ( w = <. x , x >. <-> ( w = <. x , x >. /\ x = x ) )
10	4 7 9	3bitri	|- ( E. z ( w = <. x , z >. /\ x = z ) <-> ( w = <. x , x >. /\ x = x ) )
11	10	exbii	|- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x ( w = <. x , x >. /\ x = x ) )
12		nfe1	|- F/ x E. x ( w = <. x , x >. /\ x = x )
13	12	19.9	|- ( E. x E. x ( w = <. x , x >. /\ x = x ) <-> E. x ( w = <. x , x >. /\ x = x ) )
14	11 13	bitr4i	|- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. x ( w = <. x , x >. /\ x = x ) )
15		opeq2	|- ( x = y -> <. x , x >. = <. x , y >. )
16	15	eqeq2d	|- ( x = y -> ( w = <. x , x >. <-> w = <. x , y >. ) )
17		equequ2	|- ( x = y -> ( x = x <-> x = y ) )
18	16 17	anbi12d	|- ( x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) )
19	18	sps	|- ( A. x x = y -> ( ( w = <. x , x >. /\ x = x ) <-> ( w = <. x , y >. /\ x = y ) ) )
20	19	drex1	|- ( A. x x = y -> ( E. x ( w = <. x , x >. /\ x = x ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
21	20	drex2	|- ( A. x x = y -> ( E. x E. x ( w = <. x , x >. /\ x = x ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) ) )
22	14 21	syl5bb	|- ( A. x x = y -> ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) ) )
23		nfnae	|- F/ x -. A. x x = y
24		nfnae	|- F/ y -. A. x x = y
25		nfcvd	|- ( -. A. x x = y -> F/_ y w )
26		nfcvf2	|- ( -. A. x x = y -> F/_ y x )
27		nfcvd	|- ( -. A. x x = y -> F/_ y z )
28	26 27	nfopd	|- ( -. A. x x = y -> F/_ y <. x , z >. )
29	25 28	nfeqd	|- ( -. A. x x = y -> F/ y w = <. x , z >. )
30	26 27	nfeqd	|- ( -. A. x x = y -> F/ y x = z )
31	29 30	nfand	|- ( -. A. x x = y -> F/ y ( w = <. x , z >. /\ x = z ) )
32		opeq2	|- ( z = y -> <. x , z >. = <. x , y >. )
33	32	eqeq2d	|- ( z = y -> ( w = <. x , z >. <-> w = <. x , y >. ) )
34		equequ2	|- ( z = y -> ( x = z <-> x = y ) )
35	33 34	anbi12d	|- ( z = y -> ( ( w = <. x , z >. /\ x = z ) <-> ( w = <. x , y >. /\ x = y ) ) )
36	35	a1i	|- ( -. A. x x = y -> ( z = y -> ( ( w = <. x , z >. /\ x = z ) <-> ( w = <. x , y >. /\ x = y ) ) ) )
37	24 31 36	cbvexd	|- ( -. A. x x = y -> ( E. z ( w = <. x , z >. /\ x = z ) <-> E. y ( w = <. x , y >. /\ x = y ) ) )
38	23 37	exbid	|- ( -. A. x x = y -> ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) ) )
39	22 38	pm2.61i	|- ( E. x E. z ( w = <. x , z >. /\ x = z ) <-> E. x E. y ( w = <. x , y >. /\ x = y ) )
40	39	abbii	|- { w | E. x E. z ( w = <. x , z >. /\ x = z ) } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
41		df-opab	|- { <. x , z >. | x = z } = { w | E. x E. z ( w = <. x , z >. /\ x = z ) }
42		df-opab	|- { <. x , y >. | x = y } = { w | E. x E. y ( w = <. x , y >. /\ x = y ) }
43	40 41 42	3eqtr4i	|- { <. x , z >. | x = z } = { <. x , y >. | x = y }
44	1 43	eqtri	|- _I = { <. x , y >. | x = y }