Theorem inex1 2711

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 2700	. . 3 ⊢ ∃x∀y(y ∈ x ↔ (y ∈ A ⋀ y ∈ B))
3		dfcleq 1468	. . . . 5 ⊢ (x = (A ∩ B) ↔ ∀y(y ∈ x ↔ y ∈ (A ∩ B)))
4		elin 2203	. . . . . . 7 ⊢ (y ∈ (A ∩ B) ↔ (y ∈ A ⋀ y ∈ B))
5	4	bibi2i 607	. . . . . 6 ⊢ ((y ∈ x ↔ y ∈ (A ∩ B)) ↔ (y ∈ x ↔ (y ∈ A ⋀ y ∈ B)))
6	5	albii 997	. . . . 5 ⊢ (∀y(y ∈ x ↔ y ∈ (A ∩ B)) ↔ ∀y(y ∈ x ↔ (y ∈ A ⋀ y ∈ B)))
7	3, 6	bitr 173	. . . 4 ⊢ (x = (A ∩ B) ↔ ∀y(y ∈ x ↔ (y ∈ A ⋀ y ∈ B)))
8	7	exbii 1049	. . 3 ⊢ (∃x x = (A ∩ B) ↔ ∃x∀y(y ∈ x ↔ (y ∈ A ⋀ y ∈ B)))
9	2, 8	mpbir 190	. 2 ⊢ ∃x x = (A ∩ B)
10	9	issetri 1812	1 ⊢ (A ∩ B) ∈ V

Syntax hints:   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954   ∈ wcel 956  ∃wex 978  Vcvv 1807   ∩ cin 2042

This theorem is referenced by:  inex2 2712  inex1g 2713  onfr 2981  ssimaex 3759  exfo 3813  ssenen 4490  abfii4 4544  zfregs 4627  bnd2 4704  kmlem13 4757  brdom3 4781  brdom5 4782  brdom4 4783  subbas 7594  subtop 7596  sn0top 7597  fctop 7600  cctop 7602  ntunte 10376  qusp 10466  oefil2 10477

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047

Copyright terms: Public domain