Theorem inex1 2716

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

Hypothesis

Ref	Expression
inex1.1	|- A e. V

Assertion

Ref	Expression
inex1	|- (A i^i B) e. V

Proof of Theorem inex1

Step	Hyp	Ref	Expression
1		inex1.1	. . . 4 |- A e. V
2	1	zfauscl 2705	. . 3 |- E.xA.y(y e. x <-> (y e. A /\ y e. B))
3		dfcleq 1470	. . . . 5 |- (x = (A i^i B) <-> A.y(y e. x <-> y e. (A i^i B)))
4		elin 2207	. . . . . . 7 |- (y e. (A i^i B) <-> (y e. A /\ y e. B))
5	4	bibi2i 608	. . . . . 6 |- ((y e. x <-> y e. (A i^i B)) <-> (y e. x <-> (y e. A /\ y e. B)))
6	5	albii 999	. . . . 5 |- (A.y(y e. x <-> y e. (A i^i B)) <-> A.y(y e. x <-> (y e. A /\ y e. B)))
7	3, 6	bitr 173	. . . 4 |- (x = (A i^i B) <-> A.y(y e. x <-> (y e. A /\ y e. B)))
8	7	exbii 1051	. . 3 |- (E.x x = (A i^i B) <-> E.xA.y(y e. x <-> (y e. A /\ y e. B)))
9	2, 8	mpbir 190	. 2 |- E.x x = (A i^i B)
10	9	issetri 1816	1 |- (A i^i B) e. V

Syntax hints:   <-> wb 146   /\ wa 223  A.wal 954   = wceq 956   e. wcel 958  E.wex 980  Vcvv 1811   i^i cin 2046

This theorem is referenced by:  inex2 2717  inex1g 2718  onfr 2986  ssimaex 3768  exfo 3822  ssenen 4504  abfii4OLD 4564  zfregs 4647  bnd2 4724  kmlem13 4777  brdom3 4801  brdom5 4802  brdom4 4803  subbasOLD 7644  subtop 7646  sn0top 7647  fctopOLD 7650  cctop 7652  ntunte 10439  qusp 10555  oefil2 10567  rcfpfillem4 10591  rcfpfillem4OLD 10592

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-in 2051

Copyright terms: Public domain