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 "official" definition since our definition soundness check without this requirement would be much more complex. The proof can be instructive in showing how disjoint 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) Use directly Definition df-id when sufficient, since the derivation of dfid3 is nontrivial and uses auxiliary axioms ax-10 to ax-13 . (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 z w = x z x = z 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 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 z w = x z x = z w = x x x = x
11 10 exbii x z w = x z x = z x w = x x x = x
12 nfe1 x x w = x x x = x
13 12 19.9 x x w = x x x = x x w = x x x = x
14 11 13 bitr4i x z w = x z x = z x 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 x x = y w = x x x = x w = x y x = y
20 19 drex1 x x = y x w = x x x = x y w = x y x = y
21 20 drex2 x x = y x x w = x x x = x x y w = x y x = y
22 14 21 syl5bb x x = y x z w = x z x = z x y w = x y x = y
23 nfnae x ¬ x x = y
24 nfnae y ¬ x x = y
25 nfcvd ¬ x x = y _ y w
26 nfcvf2 ¬ x x = y _ y x
27 nfcvd ¬ x x = y _ y z
28 26 27 nfopd ¬ x x = y _ y x z
29 25 28 nfeqd ¬ x x = y y w = x z
30 26 27 nfeqd ¬ x x = y y x = z
31 29 30 nfand ¬ x x = y 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 ¬ x x = y z = y w = x z x = z w = x y x = y
37 24 31 36 cbvexd ¬ x x = y z w = x z x = z y w = x y x = y
38 23 37 exbid ¬ x x = y x z w = x z x = z x y w = x y x = y
39 22 38 pm2.61i x z w = x z x = z x y w = x y x = y
40 39 abbii w | x z w = x z x = z = w | x y w = x y x = y
41 df-opab x z | x = z = w | x z w = x z x = z
42 df-opab x y | x = y = w | x 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