Theorem inex1 5260

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 5241	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2727	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3915	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1820	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 275	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1849	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 231	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3457	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3438   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-in 3906

This theorem is referenced by:  inex2  5261  inex1g  5262  inuni  5293  onfr  6354  ssimaex  6917  exfo  7048  ofmres  7926  fipwuni  9327  fisn  9328  elfiun  9331  dffi3  9332  marypha1lem  9334  epfrs  9638  tcmin  9646  bnd2  9803  kmlem13  10071  brdom3  10436  brdom5  10437  brdom4  10438  fpwwe  10555  canthwelem  10559  pwfseqlem4  10571  ingru  10724  ltweuz  13882  elrest  17345  invfval  17681  isoval  17687  isofn  17697  zeroofn  17911  zerooval  17917  catcval  18022  isacs5lem  18466  isunit  20307  isrhm  20412  rhmfn  20430  rhmval  20431  rhmsubclem1  20616  2idlval  21204  pjfval  21659  psdmul  22107  fctop  22946  cctop  22948  ppttop  22949  epttop  22951  mretopd  23034  toponmre  23035  tgrest  23101  resttopon  23103  restco  23106  ordtbas2  23133  cnrest2  23228  cnpresti  23230  cnprest  23231  cnprest2  23232  cmpsublem  23341  cmpsub  23342  connsuba  23362  1stcrest  23395  subislly  23423  cldllycmp  23437  lly1stc  23438  txrest  23573  basqtop  23653  fbssfi  23779  trfbas2  23785  snfil  23806  fgcl  23820  trfil2  23829  cfinfil  23835  csdfil  23836  supfil  23837  zfbas  23838  fin1aufil  23874  fmfnfmlem3  23898  flimrest  23925  hauspwpwf1  23929  fclsrest  23966  tmdgsum2  24038  tsmsval2  24072  tsmssubm  24085  ustuqtop2  24184  restmetu  24512  isnmhm  24688  icopnfhmeo  24895  iccpnfhmeo  24897  xrhmeo  24898  pi1buni  24994  minveclem3b  25382  uniioombllem2  25538  uniioombllem6  25543  vitali  25568  ellimc2  25832  limcflf  25836  taylfvallem  26319  taylf  26322  tayl0  26323  taylpfval  26326  xrlimcnp  26932  lrrecse  27912  ewlkle  29628  upgrewlkle2  29629  wlk1walk  29661  maprnin  32759  ordtprsval  34024  ordtprsuni  34025  ordtrestNEW  34027  ordtrest2NEWlem  34028  ordtrest2NEW  34029  ordtconnlem1  34030  xrge0iifhmeo  34042  eulerpartgbij  34478  eulerpartlemmf  34481  eulerpart  34488  ballotlemfrc  34633  cvmsss2  35417  cvmcov2  35418  mvrsval  35648  mpstval  35678  mclsind  35713  mthmpps  35725  dfon2lem4  35927  brapply  36079  neibastop1  36502  filnetlem3  36523  weiunfr  36610  bj-restn0  37234  bj-restuni  37241  ptrest  37759  heiborlem3  37953  heibor  37961  polvalN  40104  fnwe2lem2  43235  harval3  43721  superficl  43750  ssficl  43752  trficl  43852  onfrALTlem5  44725  onfrALTlem5VD  45067  fourierdlem48  46340  fourierdlem49  46341  sge0resplit  46592  hoiqssbllem3  46810  rngcvalALTV  48453  rhmsubcALTVlem1  48469  ringcvalALTV  48477  invfn  49217