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.

Step	Hyp	Ref	Expression
1		ax-pr 5432	. 2 ⊢ ∃𝑦∀𝑥((𝑥 = 𝑧 ∨ 𝑥 = 𝑧) → 𝑥 ∈ 𝑦)
2		ax6ev 1969	. . . 4 ⊢ ∃𝑥 𝑥 = 𝑧
3		pm2.07 903	. . . 4 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑧 ∨ 𝑥 = 𝑧))
4	2, 3	eximii 1837	. . 3 ⊢ ∃𝑥(𝑥 = 𝑧 ∨ 𝑥 = 𝑧)
5		exim 1834	. . 3 ⊢ (∀𝑥((𝑥 = 𝑧 ∨ 𝑥 = 𝑧) → 𝑥 ∈ 𝑦) → (∃𝑥(𝑥 = 𝑧 ∨ 𝑥 = 𝑧) → ∃𝑥 𝑥 ∈ 𝑦))
6	4, 5	mpi 20	. 2 ⊢ (∀𝑥((𝑥 = 𝑧 ∨ 𝑥 = 𝑧) → 𝑥 ∈ 𝑦) → ∃𝑥 𝑥 ∈ 𝑦)
7	1, 6	eximii 1837	1 ⊢ ∃𝑦∃𝑥 𝑥 ∈ 𝑦

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