Theorem inex1 2684

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 2673	. . 3 |- E.xA.y(y e. x <-> (y e. A /\ y e. B))
3		dfcleq 1447	. . . . 5 |- (x = (A i^i B) <-> A.y(y e. x <-> y e. (A i^i B)))
4		elin 2178	. . . . . . 7 |- (y e. (A i^i B) <-> (y e. A /\ y e. B))
5	4	bibi2i 606	. . . . . 6 |- ((y e. x <-> y e. (A i^i B)) <-> (y e. x <-> (y e. A /\ y e. B)))
6	5	albii 975	. . . . 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 1027	. . 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 1791	1 |- (A i^i B) e. V

Syntax hints:   <-> wb 146   /\ wa 223  A.wal 950  E.wex 956   = wceq 1099   e. wcel 1105  Vcvv 1786   i^i cin 2017

This theorem is referenced by:  inex2 2685  inex1g 2686  onfr 2949  ssimaex 3707  exfo 3761  ssenen 4436  abfii4 4490  zfregs 4571  bnd2 4648  kmlem13 4701  brdom3 4725  brdom5 4726  brdom4 4727  subbas 7537  subtop 7539  sn0top 7540  fctop 7543  cctop 7545  ntunte 8699  qusp 8780  oefil2 8791

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787  df-in 2022

Copyright terms: Public domain