Theorem elex2 2616

Description: If a class contains another class, then it contains some set. (Contributed by Alan Sare, 25-Sep-2011.)

Assertion

Ref	Expression
elex2	⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem elex2

Step	Hyp	Ref	Expression
1		eleq1a 2151	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1796	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2614	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1531	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 61	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1283   = wceq 1285  ∃wex 1422   ∈ wcel 1434

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-v 2604

This theorem is referenced by:  snmg  3510  oprcl  3596  exss  3984  onintrab2im  4264  regexmidlemm  4277  acexmidlem2  5534  frecabcl  6042  enm  6354  ssfilem  6400  fin0  6409  fin0or  6410  diffitest  6411  diffisn  6417  infm  6422  caucvgsrlemasr  7017  gtso  7246  indstr  8751  negm  8770  fzm  9122  fzom  9239  rexfiuz  10002  r19.2uz  10006  resqrexlemgt0  10033  climuni  10259  bezoutlembi  10527  lcmgcdlem  10592