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

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

This theorem looks similar to el 5448, but its meaning is different. It only depends on the axioms ax-mp 5 to ax-4 1806, ax-6 1965, and ax-pr 5438. 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 5445. (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 5438 . 2 𝑦𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦)
2 ax6ev 1967 . . . 4 𝑥 𝑥 = 𝑧
3 pm2.07 902 . . . 4 (𝑥 = 𝑧 → (𝑥 = 𝑧𝑥 = 𝑧))
42, 3eximii 1834 . . 3 𝑥(𝑥 = 𝑧𝑥 = 𝑧)
5 exim 1831 . . 3 (∀𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦) → (∃𝑥(𝑥 = 𝑧𝑥 = 𝑧) → ∃𝑥 𝑥𝑦))
64, 5mpi 20 . 2 (∀𝑥((𝑥 = 𝑧𝑥 = 𝑧) → 𝑥𝑦) → ∃𝑥 𝑥𝑦)
71, 6eximii 1834 1 𝑦𝑥 𝑥𝑦
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 847  wal 1535  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-6 1965  ax-pr 5438
This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1777
This theorem is referenced by:  exexneq  5445
  Copyright terms: Public domain W3C validator