Theorem inex1 5241

Description: Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
inex1.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
inex1	⊢ (𝐴 ∩ 𝐵) ∈ V

Proof of Theorem inex1

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inex1.1	. . . 4 ⊢ 𝐴 ∈ V
2	1	zfauscl 5225	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2731	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3903	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 338	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1822	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 274	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1850	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 230	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3448	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539  ∃wex 1782   ∈ wcel 2106  Vcvv 3432   ∩ cin 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894

This theorem is referenced by:  inex2  5242  inex1g  5243  inuni  5267  onfr  6305  ssimaex  6853  exfo  6981  ofmres  7827  fipwuni  9185  fisn  9186  elfiun  9189  dffi3  9190  marypha1lem  9192  epfrs  9489  tcmin  9499  bnd2  9651  kmlem13  9918  brdom3  10284  brdom5  10285  brdom4  10286  fpwwe  10402  canthwelem  10406  pwfseqlem4  10418  ingru  10571  ltweuz  13681  elrest  17138  invfval  17471  isoval  17477  isofn  17487  zeroofn  17704  zerooval  17710  catcval  17815  isacs5lem  18263  isunit  19899  isrhm  19965  2idlval  20504  pjfval  20913  fctop  22154  cctop  22156  ppttop  22157  epttop  22159  mretopd  22243  toponmre  22244  tgrest  22310  resttopon  22312  restco  22315  ordtbas2  22342  cnrest2  22437  cnpresti  22439  cnprest  22440  cnprest2  22441  cmpsublem  22550  cmpsub  22551  connsuba  22571  1stcrest  22604  subislly  22632  cldllycmp  22646  lly1stc  22647  txrest  22782  basqtop  22862  fbssfi  22988  trfbas2  22994  snfil  23015  fgcl  23029  trfil2  23038  cfinfil  23044  csdfil  23045  supfil  23046  zfbas  23047  fin1aufil  23083  fmfnfmlem3  23107  flimrest  23134  hauspwpwf1  23138  fclsrest  23175  tmdgsum2  23247  tsmsval2  23281  tsmssubm  23294  ustuqtop2  23394  restmetu  23726  isnmhm  23910  icopnfhmeo  24106  iccpnfhmeo  24108  xrhmeo  24109  pi1buni  24203  minveclem3b  24592  uniioombllem2  24747  uniioombllem6  24752  vitali  24777  ellimc2  25041  limcflf  25045  taylfvallem  25517  taylf  25520  tayl0  25521  taylpfval  25524  xrlimcnp  26118  ewlkle  27972  upgrewlkle2  27973  wlk1walk  28006  maprnin  31066  ordtprsval  31868  ordtprsuni  31869  ordtrestNEW  31871  ordtrest2NEWlem  31872  ordtrest2NEW  31873  ordtconnlem1  31874  xrge0iifhmeo  31886  eulerpartgbij  32339  eulerpartlemmf  32342  eulerpart  32349  ballotlemfrc  32493  cvmsss2  33236  cvmcov2  33237  mvrsval  33467  mpstval  33497  mclsind  33532  mthmpps  33544  dfon2lem4  33762  lrrecse  34099  brapply  34240  neibastop1  34548  filnetlem3  34569  bj-restn0  35261  bj-restuni  35268  ptrest  35776  heiborlem3  35971  heibor  35979  polvalN  37919  fnwe2lem2  40876  harval3  41145  superficl  41174  ssficl  41176  trficl  41277  onfrALTlem5  42162  onfrALTlem5VD  42505  fourierdlem48  43695  fourierdlem49  43696  sge0resplit  43944  hoiqssbllem3  44162  rhmfn  45476  rhmval  45477  rngcvalALTV  45519  ringcvalALTV  45565  rhmsubclem1  45644  rhmsubcALTVlem1  45662