MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exel Structured version   Visualization version   GIF version

Theorem exel 5434
Description: There exist two sets, one a member of the other.

This theorem looks similar to el 5438, but its meaning is different. It only depends on the axioms ax-mp 5 to ax-4 1812, ax-6 1972, and ax-pr 5428. This theorem does not exclude that these two sets could actually be one single set containing itself. That two different sets exist is proved by exexneq 5435. (Contributed by SN, 23-Dec-2024.)

Assertion
Ref Expression
exel 𝑦𝑥 𝑥𝑦
Distinct variable group:   𝑥,𝑦

Proof of Theorem exel
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 ax-pr 5428 . 2 𝑦𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦)
2 ax6ev 1974 . . . 4 𝑥 𝑥 = 𝑧
3 pm2.07 902 . . . 4 (𝑥 = 𝑧 → (𝑥 = 𝑧𝑥 = 𝑧))
42, 3eximii 1840 . . 3 𝑥(𝑥 = 𝑧𝑥 = 𝑧)
5 exim 1837 . . 3 (∀𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦) → (∃𝑥(𝑥 = 𝑧𝑥 = 𝑧) → ∃𝑥 𝑥𝑦))
64, 5mpi 20 . 2 (∀𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦) → ∃𝑥 𝑥𝑦)
71, 6eximii 1840 1 𝑦𝑥 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846  wal 1540  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-6 1972  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1783
This theorem is referenced by:  exexneq  5435
  Copyright terms: Public domain W3C validator