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

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

This theorem looks similar to el 5442, but its meaning is different. It only depends on the axioms ax-mp 5 to ax-4 1809, ax-6 1967, and ax-pr 5432. 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 5439. (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 5432 . 2 𝑦𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦)
2 ax6ev 1969 . . . 4 𝑥 𝑥 = 𝑧
3 pm2.07 903 . . . 4 (𝑥 = 𝑧 → (𝑥 = 𝑧𝑥 = 𝑧))
42, 3eximii 1837 . . 3 𝑥(𝑥 = 𝑧𝑥 = 𝑧)
5 exim 1834 . . 3 (∀𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦) → (∃𝑥(𝑥 = 𝑧𝑥 = 𝑧) → ∃𝑥 𝑥𝑦))
64, 5mpi 20 . 2 (∀𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦) → ∃𝑥 𝑥𝑦)
71, 6eximii 1837 1 𝑦𝑥 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 848  wal 1538  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-6 1967  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1780
This theorem is referenced by:  exexneq  5439
  Copyright terms: Public domain W3C validator