Metamath Proof Explorer


Theorem dtrucor3

Description: An example of how ax-5 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru in the ZF set theory. axc16nf and euae demonstrate that the violation of dtru leads to a model with only one object assuming its existence ( ax-6 ). The conclusion is also provable in the empty model ( see emptyal ). See also nf5 and nf5i for the relation between unconditional ax-5 and being not free. (Contributed by Zhi Wang, 23-Sep-2024)

Ref Expression
Hypotheses dtrucor3.1
|- -. A. x x = y
dtrucor3.2
|- ( x = y -> A. x x = y )
Assertion dtrucor3
|- A. x x = y

Proof

Step Hyp Ref Expression
1 dtrucor3.1
 |-  -. A. x x = y
2 dtrucor3.2
 |-  ( x = y -> A. x x = y )
3 ax6ev
 |-  E. x x = y
4 1 2 mto
 |-  -. x = y
5 4 nex
 |-  -. E. x x = y
6 3 5 pm2.24ii
 |-  A. x x = y