Theorem inex1 5255

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 5234	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2730	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3906	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1821	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 275	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1850	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 231	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3449	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3430   ∩ cin 3889

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897

This theorem is referenced by:  inex2  5256  inex1g  5257  inuni  5288  onfr  6357  ssimaex  6920  exfo  7052  ofmres  7931  fipwuni  9333  fisn  9334  elfiun  9337  dffi3  9338  marypha1lem  9340  epfrs  9646  tcmin  9654  bnd2  9811  kmlem13  10079  brdom3  10444  brdom5  10445  brdom4  10446  fpwwe  10563  canthwelem  10567  pwfseqlem4  10579  ingru  10732  ltweuz  13917  elrest  17384  invfval  17720  isoval  17726  isofn  17736  zeroofn  17950  zerooval  17956  catcval  18061  isacs5lem  18505  isunit  20347  isrhm  20452  rhmfn  20470  rhmval  20471  rhmsubclem1  20656  2idlval  21244  pjfval  21699  psdmul  22145  fctop  22982  cctop  22984  ppttop  22985  epttop  22987  mretopd  23070  toponmre  23071  tgrest  23137  resttopon  23139  restco  23142  ordtbas2  23169  cnrest2  23264  cnpresti  23266  cnprest  23267  cnprest2  23268  cmpsublem  23377  cmpsub  23378  connsuba  23398  1stcrest  23431  subislly  23459  cldllycmp  23473  lly1stc  23474  txrest  23609  basqtop  23689  fbssfi  23815  trfbas2  23821  snfil  23842  fgcl  23856  trfil2  23865  cfinfil  23871  csdfil  23872  supfil  23873  zfbas  23874  fin1aufil  23910  fmfnfmlem3  23934  flimrest  23961  hauspwpwf1  23965  fclsrest  24002  tmdgsum2  24074  tsmsval2  24108  tsmssubm  24121  ustuqtop2  24220  restmetu  24548  isnmhm  24724  icopnfhmeo  24923  iccpnfhmeo  24925  xrhmeo  24926  pi1buni  25020  minveclem3b  25408  uniioombllem2  25563  uniioombllem6  25568  vitali  25593  ellimc2  25857  limcflf  25861  taylfvallem  26337  taylf  26340  tayl0  26341  taylpfval  26344  xrlimcnp  26948  lrrecse  27951  ewlkle  29692  upgrewlkle2  29693  wlk1walk  29725  maprnin  32822  ordtprsval  34081  ordtprsuni  34082  ordtrestNEW  34084  ordtrest2NEWlem  34085  ordtrest2NEW  34086  ordtconnlem1  34087  xrge0iifhmeo  34099  eulerpartgbij  34535  eulerpartlemmf  34538  eulerpart  34545  ballotlemfrc  34690  cvmsss2  35475  cvmcov2  35476  mvrsval  35706  mpstval  35736  mclsind  35771  mthmpps  35783  dfon2lem4  35985  brapply  36137  neibastop1  36560  filnetlem3  36581  weiunfr  36668  bj-restn0  37421  bj-restuni  37428  ptrest  37957  heiborlem3  38151  heibor  38159  polvalN  40368  fnwe2lem2  43500  harval3  43986  superficl  44015  ssficl  44017  trficl  44117  onfrALTlem5  44990  onfrALTlem5VD  45332  fourierdlem48  46603  fourierdlem49  46604  sge0resplit  46855  hoiqssbllem3  47073  rngcvalALTV  48756  rhmsubcALTVlem1  48772  ringcvalALTV  48780  invfn  49520