Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dtrucor3 Structured version   Visualization version   GIF version

Theorem dtrucor3 45724
Description: An example of how ax-5 1917 without a distinct variable condition causes paradox in models of at least two objects. The hypothesis "dtrucor3.1" is provable from dtru 5247 in the ZF set theory. axc16nf 2264 and euae 2663 demonstrate that the violation of dtru 5247 leads to a model with only one object assuming its existence (ax-6 1975). The conclusion is also provable in the empty model ( see emptyal 1915). See also nf5 2287 and nf5i 2150 for the relation between unconditional ax-5 1917 and being not free. (Contributed by Zhi Wang, 23-Sep-2024.)
Hypotheses
Ref Expression
dtrucor3.1 ¬ ∀𝑥 𝑥 = 𝑦
dtrucor3.2 (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
Assertion
Ref Expression
dtrucor3 𝑥 𝑥 = 𝑦
Distinct variable group:   𝑥,𝑦

Proof of Theorem dtrucor3
StepHypRef Expression
1 ax6ev 1977 . 2 𝑥 𝑥 = 𝑦
2 dtrucor3.1 . . . 4 ¬ ∀𝑥 𝑥 = 𝑦
3 dtrucor3.2 . . . 4 (𝑥 = 𝑦 → ∀𝑥 𝑥 = 𝑦)
42, 3mto 200 . . 3 ¬ 𝑥 = 𝑦
54nex 1807 . 2 ¬ ∃𝑥 𝑥 = 𝑦
61, 5pm2.24ii 120 1 𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wal 1540  wex 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-6 1975
This theorem depends on definitions:  df-bi 210  df-ex 1787
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator