Theorem inex1 2790

Description: Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22.

Hypothesis

Ref	Expression
inex1.1	⊢ A ∈ V

Assertion

Ref	Expression
inex1	⊢ (A ∩ B) ∈ V

Proof of Theorem inex1

Step	Hyp	Ref	Expression
1		inex1.1	. . . 4 ⊢ A ∈ V
2	1	zfauscl 2779	. . 3 ⊢ ∃x∀y(y ∈ x ↔ (y ∈ A ⋀ y ∈ B))
3		dfcleq 1512	. . . . 5 ⊢ (x = (A ∩ B) ↔ ∀y(y ∈ x ↔ y ∈ (A ∩ B)))
4		elin 2259	. . . . . . 7 ⊢ (y ∈ (A ∩ B) ↔ (y ∈ A ⋀ y ∈ B))
5	4	bibi2i 611	. . . . . 6 ⊢ ((y ∈ x ↔ y ∈ (A ∩ B)) ↔ (y ∈ x ↔ (y ∈ A ⋀ y ∈ B)))
6	5	albii 1035	. . . . 5 ⊢ (∀y(y ∈ x ↔ y ∈ (A ∩ B)) ↔ ∀y(y ∈ x ↔ (y ∈ A ⋀ y ∈ B)))
7	3, 6	bitri 171	. . . 4 ⊢ (x = (A ∩ B) ↔ ∀y(y ∈ x ↔ (y ∈ A ⋀ y ∈ B)))
8	7	exbii 1087	. . 3 ⊢ (∃x x = (A ∩ B) ↔ ∃x∀y(y ∈ x ↔ (y ∈ A ⋀ y ∈ B)))
9	2, 8	mpbir 188	. 2 ⊢ ∃x x = (A ∩ B)
10	9	issetri 1862	1 ⊢ (A ∩ B) ∈ V

Syntax hints:   ↔ wb 144   ⋀ wa 221  ∀wal 990   = wceq 992   ∈ wcel 994  ∃wex 1016  Vcvv 1857   ∩ cin 2098

This theorem is referenced by:  inex2 2791  inex1g 2792  onfr 3014  ssimaex 3879  exfo 3936  ssenen 4651  abfii4 4707  zfregs 4793  bnd2 4870  kmlem13 4923  brdom3 4947  brdom5 4948  brdom4 4949  subbas 7856  subtop 7858  sn0top 7859  cctop 7862  ntunte 10728  toplat 10884  qusp 11068  oefil2 11079  rcfpfillem4 11092  elfiun 11421  fictblem 11422  fictb 11423  compsublem 11487  compsub 11488  neibastop1 11579  topmtcl 11586  supfil 11645  filfinnfr 11646  ufinffr 11663  ufilen 11664  filcon 11665  fmfnfmlem3 11702  filnetlem3 11765  subspabs 11903  cnss 11953  txbas 11973  txsubsp 11983  totbndss 11993  heiborlem23 12033

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-in 2103

Copyright terms: Public domain