Theorem elex2 2838

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 2310	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1927	. 2 ⊢ (𝐴 ∈ 𝐵 → ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3		elisset 2836	. 2 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 = 𝐴)
4		exim 1652	. 2 ⊢ (∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵) → (∃𝑥 𝑥 = 𝐴 → ∃𝑥 𝑥 ∈ 𝐵))
5	2, 3, 4	sylc 62	1 ⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4  ∀wal 1400   = wceq 1402  ∃wex 1545   ∈ wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  snmg  3831  oprcl  3928  brm  4181  ss1o0el1  4334  exss  4367  onintrab2im  4665  regexmidlemm  4679  reldmm  5000  dmxpid  5003  mptmex  5945  acexmidlem2  6082  elmpom  6474  frecabcl  6670  ixpm  7012  en1m  7092  dom1o  7116  dom1oi  7117  enm  7118  ssfilem  7177  ssfilemd  7179  fin0  7189  fin0or  7190  diffitest  7191  diffisn  7197  infm  7211  inffiexmid  7213  ctssdc  7454  omct  7458  ctssexmid  7491  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  acnrcl  7558  exmidaclem  7565  iftrueb01  7583  pw1if  7585  caucvgsrlemasr  8158  suplocsrlempr  8175  gtso  8405  sup3exmid  9290  indstr  10003  negm  10025  fzm  10453  fzom  10583  rexfiuz  11771  r19.2uz  11775  resqrexlemgt0  11802  climuni  12078  bezoutlembi  12801  nninfct  12837  lcmgcdlem  12874  pcprecl  13091  pc2dvds  13132  4sqlem13m  13205  nninfdclemcl  13391  dfgrp3m  13957  issubg2m  14045  issubgrpd2  14046  issubg3  14048  issubg4m  14049  grpissubg  14050  subgintm  14054  nmzsubg  14066  ghmrn  14113  ghmpreima  14122  dvdsr02  14496  01eq0ring  14580  subrgugrp  14632  lmodfopnelem1  14745  rmodislmodlem  14771  rmodislmod  14772  lss1  14783  lsssubg  14798  islss3  14800  islss4  14803  lss1d  14804  lssintclm  14805  dflidl2rng  14902  lidlsubg  14907  cnsubglem  15000  asplss  15100  aspsubrg  15102  tgioo  15746  elply2  15927  edgval  16467  wlkvtxm  16747  pw1nct  17199  rabid1o  17200  stnot  17205  nninfall  17218  nnnninfen  17230