Theorem inex1 5277

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	sepgi 5252	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2754	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3915	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 340	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1852	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 278	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1881	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 234	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3470	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3451   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906

This theorem is used by:  inex2  5278  inex1g  5279  inuni  5311  onfr  6402  ssimaex  6970  exfo  7105  ofmres  7996  fnwe2lem3  8147  fipwuni  9418  fisn  9419  elfiun  9422  dffi3  9423  marypha1lem  9425  epfrs  9732  tcmin  9740  bnd2  9956  kmlem13  10241  brdom3  10607  brdom5  10608  brdom4  10609  fpwwe  10731  canthwelem  10735  pwfseqlem4  10747  ingru  10900  ltweuz  14104  elrest  17598  invfval  17934  isoval  17940  isofn  17950  zeroofn  18164  zerooval  18170  catcval  18275  isacs5lem  18719  isunit  20603  isrhm  20709  rhmfn  20736  rhmval  20738  rhmsubclem1  20937  2idlval  21544  pjfval  22012  psdmul  22487  fctop  23322  cctop  23324  ppttop  23325  epttop  23327  mretopd  23410  toponmre  23411  tgrest  23477  resttopon  23479  restco  23482  ordtbas2  23509  cnrest2  23604  cnpresti  23606  cnprest  23607  cnprest2  23608  cmpsublem  23717  cmpsub  23718  connsuba  23738  1stcrest  23771  subislly  23800  cldllycmp  23814  lly1stc  23815  txrest  23950  basqtop  24030  fbssfi  24156  trfbas2  24162  snfil  24183  fgcl  24197  trfil2  24206  cfinfil  24212  csdfil  24213  supfil  24214  zfbas  24215  fin1aufil  24251  fmfnfmlem3  24275  flimrest  24302  hauspwpwf1  24306  fclsrest  24343  tmdgsum2  24415  tsmsval2  24449  tsmssubm  24462  ustuqtop2  24561  restmetu  24889  isnmhm  25065  icopnfhmeo  25264  iccpnfhmeo  25266  xrhmeo  25267  pi1buni  25361  minveclem3b  25749  uniioombllem2  25904  uniioombllem6  25909  vitali  25934  ellimc2  26197  limcflf  26201  taylfvallem  26685  taylf  26688  tayl0  26689  taylpfval  26692  xrlimcnp  27296  lrrecse  28328  ewlkle  30186  upgrewlkle2  30187  wlk1walk  30219  maprnin  33323  ordtprsval  34550  ordtprsuni  34551  ordtrestNEW  34553  ordtrest2NEWlem  34554  ordtrest2NEW  34555  ordtconnlem1  34556  xrge0iifhmeo  34568  eulerpartgbij  35004  eulerpartlemmf  35007  eulerpart  35014  ballotlemfrc  35159  weexenwe  35756  cvmsss2  36039  cvmcov2  36040  mvrsval  36270  mpstval  36300  mclsind  36335  mthmpps  36347  dfon2lem4  36548  brapply  36700  neibastop1  37147  filnetlem3  37168  weiunfr  37255  bj-restn0  38011  bj-restuni  38018  ptrest  38537  heiborlem3  38747  heibor  38755  polvalN  40962  harval3  44538  superficl  44567  ssficl  44569  trficl  44668  onfrALTlem5  45524  onfrALTlem5VD  45866  fourierdlem48  47163  fourierdlem49  47164  sge0resplit  47415  hoiqssbllem3  47633  rngcvalALTV  49361  rhmsubcALTVlem1  49377  ringcvalALTV  49385  invfn  50137