Theorem inex1 5288

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 5263	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2762	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3929	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 340	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1846	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 278	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1875	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 234	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3482	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 209   ∧ wa 400  ∀wal 1565   = wceq 1567  ∃wex 1806   ∈ wcel 2149  Vcvv 3463   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920

This theorem is referenced by:  inex2  5289  inex1g  5290  inuni  5321  onfr  6401  ssimaex  6967  exfo  7101  ofmres  7981  fipwuni  9386  fisn  9387  elfiun  9390  dffi3  9391  marypha1lem  9393  epfrs  9700  tcmin  9708  bnd2  9879  kmlem13  10146  brdom3  10512  brdom5  10513  brdom4  10514  fpwwe  10631  canthwelem  10635  pwfseqlem4  10647  ingru  10800  ltweuz  13997  elrest  17480  invfval  17816  isoval  17822  isofn  17832  zeroofn  18046  zerooval  18052  catcval  18157  isacs5lem  18601  isunit  20455  isrhm  20560  rhmfn  20581  rhmval  20582  rhmsubclem1  20770  2idlval  21361  pjfval  21825  psdmul  22298  fctop  23130  cctop  23132  ppttop  23133  epttop  23135  mretopd  23218  toponmre  23219  tgrest  23285  resttopon  23287  restco  23290  ordtbas2  23317  cnrest2  23412  cnpresti  23414  cnprest  23415  cnprest2  23416  cmpsublem  23525  cmpsub  23526  connsuba  23546  1stcrest  23579  subislly  23607  cldllycmp  23621  lly1stc  23622  txrest  23757  basqtop  23837  fbssfi  23963  trfbas2  23969  snfil  23990  fgcl  24004  trfil2  24013  cfinfil  24019  csdfil  24020  supfil  24021  zfbas  24022  fin1aufil  24058  fmfnfmlem3  24082  flimrest  24109  hauspwpwf1  24113  fclsrest  24150  tmdgsum2  24222  tsmsval2  24256  tsmssubm  24269  ustuqtop2  24368  restmetu  24696  isnmhm  24872  icopnfhmeo  25071  iccpnfhmeo  25073  xrhmeo  25074  pi1buni  25168  minveclem3b  25556  uniioombllem2  25711  uniioombllem6  25716  vitali  25741  ellimc2  26005  limcflf  26009  taylfvallem  26487  taylf  26490  tayl0  26491  taylpfval  26494  xrlimcnp  27099  lrrecse  28101  ewlkle  29896  upgrewlkle2  29897  wlk1walk  29929  maprnin  33017  ordtprsval  34253  ordtprsuni  34254  ordtrestNEW  34256  ordtrest2NEWlem  34257  ordtrest2NEW  34258  ordtconnlem1  34259  xrge0iifhmeo  34271  eulerpartgbij  34707  eulerpartlemmf  34710  eulerpart  34717  ballotlemfrc  34862  cvmsss2  35665  cvmcov2  35666  mvrsval  35896  mpstval  35926  mclsind  35961  mthmpps  35973  dfon2lem4  36175  brapply  36327  neibastop1  36759  filnetlem3  36780  weiunfr  36867  bj-restn0  37620  bj-restuni  37627  ptrest  38158  heiborlem3  38352  heibor  38360  polvalN  40569  fnwe2lem2  43670  harval3  44156  superficl  44185  ssficl  44187  trficl  44287  onfrALTlem5  45143  onfrALTlem5VD  45485  fourierdlem48  46760  fourierdlem49  46761  sge0resplit  47012  hoiqssbllem3  47230  rngcvalALTV  48919  rhmsubcALTVlem1  48935  ringcvalALTV  48943  invfn  49693