Theorem elex2 2820

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 2303	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1922	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2818	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1648	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4  ∀wal 1396   = wceq 1398  ∃wex 1541   ∈ wcel 2202

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2805

This theorem is referenced by:  snmg  3794  oprcl  3891  brm  4144  ss1o0el1  4293  exss  4325  onintrab2im  4622  regexmidlemm  4636  reldmm  4956  dmxpid  4959  acexmidlem2  6025  elmpom  6412  frecabcl  6608  ixpm  6942  en1m  7022  dom1o  7045  dom1oi  7046  enm  7047  ssfilem  7105  ssfilemd  7107  fin0  7117  fin0or  7118  diffitest  7119  diffisn  7125  infm  7139  inffiexmid  7141  ctssdc  7355  omct  7359  ctssexmid  7392  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  acnrcl  7459  exmidaclem  7466  iftrueb01  7484  pw1if  7486  caucvgsrlemasr  8053  suplocsrlempr  8070  gtso  8300  sup3exmid  9179  indstr  9871  negm  9893  fzm  10318  fzom  10445  rexfiuz  11612  r19.2uz  11616  resqrexlemgt0  11643  climuni  11916  bezoutlembi  12639  nninfct  12675  lcmgcdlem  12712  pcprecl  12925  pc2dvds  12966  4sqlem13m  13039  nninfdclemcl  13132  dfgrp3m  13745  issubg2m  13839  issubgrpd2  13840  issubg3  13842  issubg4m  13843  grpissubg  13844  subgintm  13848  nmzsubg  13860  ghmrn  13907  ghmpreima  13916  dvdsr02  14183  01eq0ring  14267  subrgugrp  14318  lmodfopnelem1  14403  rmodislmodlem  14429  rmodislmod  14430  lss1  14441  lsssubg  14456  islss3  14458  islss4  14461  lss1d  14462  lssintclm  14463  dflidl2rng  14560  lidlsubg  14565  cnsubglem  14658  tgioo  15348  elply2  15529  edgval  15984  wlkvtxm  16264  pw1nct  16708  nninfall  16718  nnnninfen  16730