Theorem elex2 2657

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 2171	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1813	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2655	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1546	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1297   = wceq 1299  ∃wex 1436   ∈ wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-v 2643

This theorem is referenced by:  snmg  3588  oprcl  3676  exmid01  4061  exss  4087  onintrab2im  4372  regexmidlemm  4385  dmxpid  4698  acexmidlem2  5703  frecabcl  6226  ixpm  6554  enm  6643  ssfilem  6698  fin0  6708  fin0or  6709  diffitest  6710  diffisn  6716  infm  6727  inffiexmid  6729  ctssdc  6912  ctssexmid  6936  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  caucvgsrlemasr  7485  gtso  7714  sup3exmid  8573  indstr  9238  negm  9257  fzm  9659  fzom  9782  rexfiuz  10601  r19.2uz  10605  resqrexlemgt0  10632  climuni  10901  bezoutlembi  11486  lcmgcdlem  11551  tgioo  12465  nninfall  12788