Theorem inex1 5284

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 5258	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2756	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 4096	. . . . . . 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 3473	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-in 4094

This theorem is used by:  inex2  5285  inex1g  5286  inuni  5318  onfr  6428  ssimaex  7001  exfo  7137  ofmres  8030  fnwe2lem3  8184  fipwuni  9455  fisn  9456  elfiun  9459  dffi3  9460  marypha1lem  9462  epfrs  9769  tcmin  9777  bnd2  9993  kmlem13  10280  brdom3  10646  brdom5  10647  brdom4  10648  fpwwe  10770  canthwelem  10774  pwfseqlem4  10786  ingru  10939  ltweuz  14144  elrest  17648  invfval  17984  isoval  17990  isofn  18000  zeroofn  18214  zerooval  18220  catcval  18325  isacs5lem  18769  isunit  20654  isrhm  20760  rhmfn  20787  rhmval  20789  rhmsubclem1  20988  2idlval  21595  pjfval  22067  psdmul  22542  fctop  23377  cctop  23379  ppttop  23380  epttop  23382  mretopd  23465  toponmre  23466  tgrest  23532  resttopon  23534  restco  23537  ordtbas2  23564  cnrest2  23659  cnpresti  23661  cnprest  23662  cnprest2  23663  cmpsublem  23772  cmpsub  23773  connsuba  23793  1stcrest  23826  subislly  23855  cldllycmp  23869  lly1stc  23870  txrest  24005  basqtop  24085  fbssfi  24211  trfbas2  24217  snfil  24238  fgcl  24252  trfil2  24261  cfinfil  24267  csdfil  24268  supfil  24269  zfbas  24270  fin1aufil  24306  fmfnfmlem3  24330  flimrest  24357  hauspwpwf1  24361  fclsrest  24398  tmdgsum2  24470  tsmsval2  24504  tsmssubm  24517  ustuqtop2  24616  restmetu  24944  isnmhm  25120  icopnfhmeo  25319  iccpnfhmeo  25321  xrhmeo  25322  pi1buni  25416  minveclem3b  25804  uniioombllem2  25959  uniioombllem6  25964  vitali  25989  ellimc2  26252  limcflf  26256  taylfvallem  26742  taylf  26745  tayl0  26746  taylpfval  26749  xrlimcnp  27353  lrrecse  28385  ewlkle  30243  upgrewlkle2  30244  wlk1walk  30276  maprnin  33419  ordtprsval  34661  ordtprsuni  34662  ordtrestNEW  34664  ordtrest2NEWlem  34665  ordtrest2NEW  34666  ordtconnlem1  34667  xrge0iifhmeo  34679  eulerpartgbij  35115  eulerpartlemmf  35118  eulerpart  35125  ballotlemfrc  35270  weexenwe  35889  cvmsss2  36247  cvmcov2  36248  mvrsval  36478  mpstval  36508  mclsind  36543  mthmpps  36555  dfon2lem4  36763  brapply  36915  neibastop1  37362  filnetlem3  37383  weiunfr  37470  bj-restn0  38281  bj-restuni  38288  ptrest  38805  heiborlem3  39013  heibor  39021  polvalN  41228  harval3  44800  superficl  44829  ssficl  44831  trficl  44930  onfrALTlem5  45785  onfrALTlem5VD  46127  fourierdlem48  47437  fourierdlem49  47438  sge0resplit  47689  hoiqssbllem3  47907  rngcvalALTV  49635  rhmsubcALTVlem1  49651  ringcvalALTV  49659  invfn  50475