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

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

This theorem looks similar to el 5437, but its meaning is different. It only depends on the axioms ax-mp 5 to ax-4 1811, ax-6 1971, and ax-pr 5427. 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 5434. (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 5427 . 2 𝑦𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦)
2 ax6ev 1973 . . . 4 𝑥 𝑥 = 𝑧
3 pm2.07 901 . . . 4 (𝑥 = 𝑧 → (𝑥 = 𝑧𝑥 = 𝑧))
42, 3eximii 1839 . . 3 𝑥(𝑥 = 𝑧𝑥 = 𝑧)
5 exim 1836 . . 3 (∀𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦) → (∃𝑥(𝑥 = 𝑧𝑥 = 𝑧) → ∃𝑥 𝑥𝑦))
64, 5mpi 20 . 2 (∀𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦) → ∃𝑥 𝑥𝑦)
71, 6eximii 1839 1 𝑦𝑥 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 845  wal 1539  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-6 1971  ax-pr 5427
This theorem depends on definitions:  df-bi 206  df-or 846  df-ex 1782
This theorem is referenced by:  exexneq  5434
  Copyright terms: Public domain W3C validator