Metamath Proof Explorer


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=xy|x=y

Proof

Step Hyp Ref Expression
1 df-id I=xz|x=z
2 equcom x=zz=x
3 2 anbi1ci w=xzx=zz=xw=xz
4 3 exbii zw=xzx=zzz=xw=xz
5 opeq2 z=xxz=xx
6 5 eqeq2d z=xw=xzw=xx
7 6 equsexvw zz=xw=xzw=xx
8 equid x=x
9 8 biantru w=xxw=xxx=x
10 4 7 9 3bitri zw=xzx=zw=xxx=x
11 10 exbii xzw=xzx=zxw=xxx=x
12 nfe1 xxw=xxx=x
13 12 19.9 xxw=xxx=xxw=xxx=x
14 11 13 bitr4i xzw=xzx=zxxw=xxx=x
15 opeq2 x=yxx=xy
16 15 eqeq2d x=yw=xxw=xy
17 equequ2 x=yx=xx=y
18 16 17 anbi12d x=yw=xxx=xw=xyx=y
19 18 sps xx=yw=xxx=xw=xyx=y
20 19 drex1 xx=yxw=xxx=xyw=xyx=y
21 20 drex2 xx=yxxw=xxx=xxyw=xyx=y
22 14 21 bitrid xx=yxzw=xzx=zxyw=xyx=y
23 nfnae x¬xx=y
24 nfnae y¬xx=y
25 nfcvd ¬xx=y_yw
26 nfcvf2 ¬xx=y_yx
27 nfcvd ¬xx=y_yz
28 26 27 nfopd ¬xx=y_yxz
29 25 28 nfeqd ¬xx=yyw=xz
30 26 27 nfeqd ¬xx=yyx=z
31 29 30 nfand ¬xx=yyw=xzx=z
32 opeq2 z=yxz=xy
33 32 eqeq2d z=yw=xzw=xy
34 equequ2 z=yx=zx=y
35 33 34 anbi12d z=yw=xzx=zw=xyx=y
36 35 a1i ¬xx=yz=yw=xzx=zw=xyx=y
37 24 31 36 cbvexd ¬xx=yzw=xzx=zyw=xyx=y
38 23 37 exbid ¬xx=yxzw=xzx=zxyw=xyx=y
39 22 38 pm2.61i xzw=xzx=zxyw=xyx=y
40 39 abbii w|xzw=xzx=z=w|xyw=xyx=y
41 df-opab xz|x=z=w|xzw=xzx=z
42 df-opab xy|x=y=w|xyw=xyx=y
43 40 41 42 3eqtr4i xz|x=z=xy|x=y
44 1 43 eqtri I=xy|x=y