Theorem elex2 2746

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 2242	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1867	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2744	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1592	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1346   = wceq 1348  ∃wex 1485   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732

This theorem is referenced by:  snmg  3699  oprcl  3787  brm  4037  ss1o0el1  4181  exss  4210  onintrab2im  4500  regexmidlemm  4514  dmxpid  4830  acexmidlem2  5848  frecabcl  6376  ixpm  6706  enm  6796  ssfilem  6851  fin0  6861  fin0or  6862  diffitest  6863  diffisn  6869  infm  6880  inffiexmid  6882  ctssdc  7088  omct  7092  ctssexmid  7124  exmidfodomrlemr  7172  exmidfodomrlemrALT  7173  exmidaclem  7178  caucvgsrlemasr  7745  suplocsrlempr  7762  gtso  7991  sup3exmid  8866  indstr  9545  negm  9567  fzm  9987  fzom  10113  rexfiuz  10946  r19.2uz  10950  resqrexlemgt0  10977  climuni  11249  bezoutlembi  11953  lcmgcdlem  12024  pcprecl  12236  pc2dvds  12276  nninfdclemcl  12396  tgioo  13305  pw1nct  14001  nninfall  14007