Theorem inex1 5185

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 5169	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2792	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3897	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 341	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1821	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 278	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1849	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 234	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3457	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2111  Vcvv 3441   ∩ cin 3880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-sep 5167

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888

This theorem is referenced by:  inex2  5186  inex1g  5187  inuni  5210  predasetex  6131  onfr  6198  ssimaex  6723  exfo  6848  ofmres  7667  fipwuni  8874  fisn  8875  elfiun  8878  dffi3  8879  marypha1lem  8881  epfrs  9157  tcmin  9167  bnd2  9306  kmlem13  9573  brdom3  9939  brdom5  9940  brdom4  9941  fpwwe  10057  canthwelem  10061  pwfseqlem4  10073  ingru  10226  ltweuz  13324  elrest  16693  invfval  17021  isoval  17027  isofn  17037  zerooval  17251  catcval  17348  isacs5lem  17771  isunit  19403  isrhm  19469  2idlval  19999  pjfval  20395  fctop  21609  cctop  21611  ppttop  21612  epttop  21614  mretopd  21697  toponmre  21698  tgrest  21764  resttopon  21766  restco  21769  ordtbas2  21796  cnrest2  21891  cnpresti  21893  cnprest  21894  cnprest2  21895  cmpsublem  22004  cmpsub  22005  connsuba  22025  1stcrest  22058  subislly  22086  cldllycmp  22100  lly1stc  22101  txrest  22236  basqtop  22316  fbssfi  22442  trfbas2  22448  snfil  22469  fgcl  22483  trfil2  22492  cfinfil  22498  csdfil  22499  supfil  22500  zfbas  22501  fin1aufil  22537  fmfnfmlem3  22561  flimrest  22588  hauspwpwf1  22592  fclsrest  22629  tmdgsum2  22701  tsmsval2  22735  tsmssubm  22748  ustuqtop2  22848  restmetu  23177  isnmhm  23352  icopnfhmeo  23548  iccpnfhmeo  23550  xrhmeo  23551  pi1buni  23645  minveclem3b  24032  uniioombllem2  24187  uniioombllem6  24192  vitali  24217  ellimc2  24480  limcflf  24484  taylfvallem  24953  taylf  24956  tayl0  24957  taylpfval  24960  xrlimcnp  25554  ewlkle  27395  upgrewlkle2  27396  wlk1walk  27428  maprnin  30493  ordtprsval  31271  ordtprsuni  31272  ordtrestNEW  31274  ordtrest2NEWlem  31275  ordtrest2NEW  31276  ordtconnlem1  31277  xrge0iifhmeo  31289  eulerpartgbij  31740  eulerpartlemmf  31743  eulerpart  31750  ballotlemfrc  31894  cvmsss2  32634  cvmcov2  32635  mvrsval  32865  mpstval  32895  mclsind  32930  mthmpps  32942  dfon2lem4  33144  brapply  33512  neibastop1  33820  filnetlem3  33841  bj-restn0  34505  bj-restuni  34512  ptrest  35056  heiborlem3  35251  heibor  35259  polvalN  37201  fnwe2lem2  39995  harval3  40244  superficl  40266  ssficl  40268  trficl  40370  onfrALTlem5  41248  onfrALTlem5VD  41591  fourierdlem48  42796  fourierdlem49  42797  sge0resplit  43045  hoiqssbllem3  43263  rhmfn  44542  rhmval  44543  rngcvalALTV  44585  ringcvalALTV  44631  rhmsubclem1  44710  rhmsubcALTVlem1  44728