Theorem inex1 5316

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 5300	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2725	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3963	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1821	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 274	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1850	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 230	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3490	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 205   ∧ wa 396  ∀wal 1539   = wceq 1541  ∃wex 1781   ∈ wcel 2106  Vcvv 3474   ∩ cin 3946

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954

This theorem is referenced by:  inex2  5317  inex1g  5318  inuni  5342  onfr  6400  ssimaex  6973  exfo  7103  ofmres  7967  fipwuni  9417  fisn  9418  elfiun  9421  dffi3  9422  marypha1lem  9424  epfrs  9722  tcmin  9732  bnd2  9884  kmlem13  10153  brdom3  10519  brdom5  10520  brdom4  10521  fpwwe  10637  canthwelem  10641  pwfseqlem4  10653  ingru  10806  ltweuz  13922  elrest  17369  invfval  17702  isoval  17708  isofn  17718  zeroofn  17935  zerooval  17941  catcval  18046  isacs5lem  18494  isunit  20179  isrhm  20249  2idlval  20850  pjfval  21252  fctop  22498  cctop  22500  ppttop  22501  epttop  22503  mretopd  22587  toponmre  22588  tgrest  22654  resttopon  22656  restco  22659  ordtbas2  22686  cnrest2  22781  cnpresti  22783  cnprest  22784  cnprest2  22785  cmpsublem  22894  cmpsub  22895  connsuba  22915  1stcrest  22948  subislly  22976  cldllycmp  22990  lly1stc  22991  txrest  23126  basqtop  23206  fbssfi  23332  trfbas2  23338  snfil  23359  fgcl  23373  trfil2  23382  cfinfil  23388  csdfil  23389  supfil  23390  zfbas  23391  fin1aufil  23427  fmfnfmlem3  23451  flimrest  23478  hauspwpwf1  23482  fclsrest  23519  tmdgsum2  23591  tsmsval2  23625  tsmssubm  23638  ustuqtop2  23738  restmetu  24070  isnmhm  24254  icopnfhmeo  24450  iccpnfhmeo  24452  xrhmeo  24453  pi1buni  24547  minveclem3b  24936  uniioombllem2  25091  uniioombllem6  25096  vitali  25121  ellimc2  25385  limcflf  25389  taylfvallem  25861  taylf  25864  tayl0  25865  taylpfval  25868  xrlimcnp  26462  lrrecse  27415  ewlkle  28851  upgrewlkle2  28852  wlk1walk  28885  maprnin  31943  ordtprsval  32886  ordtprsuni  32887  ordtrestNEW  32889  ordtrest2NEWlem  32890  ordtrest2NEW  32891  ordtconnlem1  32892  xrge0iifhmeo  32904  eulerpartgbij  33359  eulerpartlemmf  33362  eulerpart  33369  ballotlemfrc  33513  cvmsss2  34253  cvmcov2  34254  mvrsval  34484  mpstval  34514  mclsind  34549  mthmpps  34561  dfon2lem4  34746  brapply  34898  neibastop1  35232  filnetlem3  35253  bj-restn0  35959  bj-restuni  35966  ptrest  36475  heiborlem3  36669  heibor  36677  polvalN  38764  fnwe2lem2  41778  harval3  42274  superficl  42303  ssficl  42305  trficl  42405  onfrALTlem5  43288  onfrALTlem5VD  43631  fourierdlem48  44856  fourierdlem49  44857  sge0resplit  45108  hoiqssbllem3  45326  rhmfn  46705  rhmval  46706  rngcvalALTV  46812  ringcvalALTV  46858  rhmsubclem1  46937  rhmsubcALTVlem1  46955