Theorem inex1 5223

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 5207	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2817	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 4171	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 340	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1820	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 277	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1848	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 233	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3512	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 208   ∧ wa 398  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114  Vcvv 3496   ∩ cin 3937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945

This theorem is referenced by:  inex2  5224  inex1g  5225  inuni  5248  predasetex  6165  onfr  6232  ssimaex  6750  exfo  6873  ofmres  7687  fipwuni  8892  fisn  8893  elfiun  8896  dffi3  8897  marypha1lem  8899  epfrs  9175  tcmin  9185  bnd2  9324  kmlem13  9590  brdom3  9952  brdom5  9953  brdom4  9954  fpwwe  10070  canthwelem  10074  pwfseqlem4  10086  ingru  10239  ltweuz  13332  elrest  16703  invfval  17031  isoval  17037  isofn  17047  zerooval  17261  catcval  17358  isacs5lem  17781  isunit  19409  isrhm  19475  2idlval  20008  pjfval  20852  fctop  21614  cctop  21616  ppttop  21617  epttop  21619  mretopd  21702  toponmre  21703  tgrest  21769  resttopon  21771  restco  21774  ordtbas2  21801  cnrest2  21896  cnpresti  21898  cnprest  21899  cnprest2  21900  cmpsublem  22009  cmpsub  22010  connsuba  22030  1stcrest  22063  subislly  22091  cldllycmp  22105  lly1stc  22106  txrest  22241  basqtop  22321  fbssfi  22447  trfbas2  22453  snfil  22474  fgcl  22488  trfil2  22497  cfinfil  22503  csdfil  22504  supfil  22505  zfbas  22506  fin1aufil  22542  fmfnfmlem3  22566  flimrest  22593  hauspwpwf1  22597  fclsrest  22634  tmdgsum2  22706  tsmsval2  22740  tsmssubm  22753  ustuqtop2  22853  restmetu  23182  isnmhm  23357  icopnfhmeo  23549  iccpnfhmeo  23551  xrhmeo  23552  pi1buni  23646  minveclem3b  24033  uniioombllem2  24186  uniioombllem6  24191  vitali  24216  ellimc2  24477  limcflf  24481  taylfvallem  24948  taylf  24951  tayl0  24952  taylpfval  24955  xrlimcnp  25548  ewlkle  27389  upgrewlkle2  27390  wlk1walk  27422  maprnin  30469  ordtprsval  31163  ordtprsuni  31164  ordtrestNEW  31166  ordtrest2NEWlem  31167  ordtrest2NEW  31168  ordtconnlem1  31169  xrge0iifhmeo  31181  eulerpartgbij  31632  eulerpartlemmf  31635  eulerpart  31642  ballotlemfrc  31786  cvmsss2  32523  cvmcov2  32524  mvrsval  32754  mpstval  32784  mclsind  32819  mthmpps  32831  dfon2lem4  33033  brapply  33401  neibastop1  33709  filnetlem3  33730  bj-restn0  34383  bj-restuni  34390  ptrest  34893  heiborlem3  35093  heibor  35101  polvalN  37043  fnwe2lem2  39658  harval3  39911  superficl  39933  ssficl  39935  trficl  40021  onfrALTlem5  40883  onfrALTlem5VD  41226  fourierdlem48  42446  fourierdlem49  42447  sge0resplit  42695  hoiqssbllem3  42913  rhmfn  44196  rhmval  44197  rngcvalALTV  44239  ringcvalALTV  44285  rhmsubclem1  44364  rhmsubcALTVlem1  44382