Theorem inex1 5245

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 5220	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2732	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3899	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 338	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1826	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 276	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1855	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 232	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3450	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 207   ∧ wa 396  ∀wal 1545   = wceq 1547  ∃wex 1786   ∈ wcel 2119  Vcvv 3431   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890

This theorem is referenced by:  inex2  5246  inex1g  5247  inuni  5278  onfr  6349  ssimaex  6912  exfo  7046  ofmres  7926  fipwuni  9329  fisn  9330  elfiun  9333  dffi3  9334  marypha1lem  9336  epfrs  9643  tcmin  9651  bnd2  9808  kmlem13  10076  brdom3  10441  brdom5  10442  brdom4  10443  fpwwe  10560  canthwelem  10564  pwfseqlem4  10576  ingru  10729  ltweuz  13914  elrest  17381  invfval  17717  isoval  17723  isofn  17733  zeroofn  17947  zerooval  17953  catcval  18058  isacs5lem  18502  isunit  20344  isrhm  20449  rhmfn  20470  rhmval  20471  rhmsubclem1  20657  2idlval  21244  pjfval  21681  psdmul  22154  fctop  22987  cctop  22989  ppttop  22990  epttop  22992  mretopd  23075  toponmre  23076  tgrest  23142  resttopon  23144  restco  23147  ordtbas2  23174  cnrest2  23269  cnpresti  23271  cnprest  23272  cnprest2  23273  cmpsublem  23382  cmpsub  23383  connsuba  23403  1stcrest  23436  subislly  23464  cldllycmp  23478  lly1stc  23479  txrest  23614  basqtop  23694  fbssfi  23820  trfbas2  23826  snfil  23847  fgcl  23861  trfil2  23870  cfinfil  23876  csdfil  23877  supfil  23878  zfbas  23879  fin1aufil  23915  fmfnfmlem3  23939  flimrest  23966  hauspwpwf1  23970  fclsrest  24007  tmdgsum2  24079  tsmsval2  24113  tsmssubm  24126  ustuqtop2  24225  restmetu  24553  isnmhm  24729  icopnfhmeo  24928  iccpnfhmeo  24930  xrhmeo  24931  pi1buni  25025  minveclem3b  25413  uniioombllem2  25568  uniioombllem6  25573  vitali  25598  ellimc2  25862  limcflf  25866  taylfvallem  26341  taylf  26344  tayl0  26345  taylpfval  26348  xrlimcnp  26950  lrrecse  27952  ewlkle  29692  upgrewlkle2  29693  wlk1walk  29725  maprnin  32823  ordtprsval  34102  ordtprsuni  34103  ordtrestNEW  34105  ordtrest2NEWlem  34106  ordtrest2NEW  34107  ordtconnlem1  34108  xrge0iifhmeo  34120  eulerpartgbij  34556  eulerpartlemmf  34559  eulerpart  34566  ballotlemfrc  34711  cvmsss2  35502  cvmcov2  35503  mvrsval  35733  mpstval  35763  mclsind  35798  mthmpps  35810  dfon2lem4  36012  brapply  36164  neibastop1  36587  filnetlem3  36608  weiunfr  36695  bj-restn0  37448  bj-restuni  37455  ptrest  37986  heiborlem3  38180  heibor  38188  polvalN  40397  fnwe2lem2  43496  harval3  43982  superficl  44011  ssficl  44013  trficl  44113  onfrALTlem5  44986  onfrALTlem5VD  45328  fourierdlem48  46597  fourierdlem49  46598  sge0resplit  46849  hoiqssbllem3  47067  rngcvalALTV  48756  rhmsubcALTVlem1  48772  ringcvalALTV  48780  invfn  49520