Theorem inex1 5308

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 5292	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2717	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3957	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1813	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 275	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1842	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 230	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3483	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 205   ∧ wa 395  ∀wal 1531   = wceq 1533  ∃wex 1773   ∈ wcel 2098  Vcvv 3466   ∩ cin 3940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-sep 5290

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3948

This theorem is referenced by:  inex2  5309  inex1g  5310  inuni  5334  onfr  6394  ssimaex  6967  exfo  7097  ofmres  7965  fipwuni  9418  fisn  9419  elfiun  9422  dffi3  9423  marypha1lem  9425  epfrs  9723  tcmin  9733  bnd2  9885  kmlem13  10154  brdom3  10520  brdom5  10521  brdom4  10522  fpwwe  10638  canthwelem  10642  pwfseqlem4  10654  ingru  10807  ltweuz  13927  elrest  17378  invfval  17711  isoval  17717  isofn  17727  zeroofn  17947  zerooval  17953  catcval  18058  isacs5lem  18506  isunit  20271  isrhm  20376  rhmfn  20397  rhmval  20398  rhmsubclem1  20577  2idlval  21104  pjfval  21590  fctop  22851  cctop  22853  ppttop  22854  epttop  22856  mretopd  22940  toponmre  22941  tgrest  23007  resttopon  23009  restco  23012  ordtbas2  23039  cnrest2  23134  cnpresti  23136  cnprest  23137  cnprest2  23138  cmpsublem  23247  cmpsub  23248  connsuba  23268  1stcrest  23301  subislly  23329  cldllycmp  23343  lly1stc  23344  txrest  23479  basqtop  23559  fbssfi  23685  trfbas2  23691  snfil  23712  fgcl  23726  trfil2  23735  cfinfil  23741  csdfil  23742  supfil  23743  zfbas  23744  fin1aufil  23780  fmfnfmlem3  23804  flimrest  23831  hauspwpwf1  23835  fclsrest  23872  tmdgsum2  23944  tsmsval2  23978  tsmssubm  23991  ustuqtop2  24091  restmetu  24423  isnmhm  24607  icopnfhmeo  24812  iccpnfhmeo  24814  xrhmeo  24815  pi1buni  24911  minveclem3b  25300  uniioombllem2  25456  uniioombllem6  25461  vitali  25486  ellimc2  25750  limcflf  25754  taylfvallem  26235  taylf  26238  tayl0  26239  taylpfval  26242  xrlimcnp  26841  lrrecse  27800  ewlkle  29357  upgrewlkle2  29358  wlk1walk  29391  maprnin  32451  ordtprsval  33418  ordtprsuni  33419  ordtrestNEW  33421  ordtrest2NEWlem  33422  ordtrest2NEW  33423  ordtconnlem1  33424  xrge0iifhmeo  33436  eulerpartgbij  33891  eulerpartlemmf  33894  eulerpart  33901  ballotlemfrc  34045  cvmsss2  34783  cvmcov2  34784  mvrsval  35014  mpstval  35044  mclsind  35079  mthmpps  35091  dfon2lem4  35281  brapply  35433  neibastop1  35745  filnetlem3  35766  bj-restn0  36472  bj-restuni  36479  ptrest  36991  heiborlem3  37185  heibor  37193  polvalN  39280  fnwe2lem2  42345  harval3  42839  superficl  42868  ssficl  42870  trficl  42970  onfrALTlem5  43853  onfrALTlem5VD  44196  fourierdlem48  45416  fourierdlem49  45417  sge0resplit  45668  hoiqssbllem3  45886  rngcvalALTV  47189  rhmsubcALTVlem1  47205  ringcvalALTV  47213