Theorem inex1 5322

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1534   = wceq 1536  ∃wex 1775   ∈ wcel 2105  Vcvv 3477   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969

This theorem is referenced by:  inex2  5323  inex1g  5324  inuni  5355  onfr  6424  ssimaex  6993  exfo  7124  ofmres  8007  fipwuni  9463  fisn  9464  elfiun  9467  dffi3  9468  marypha1lem  9470  epfrs  9768  tcmin  9778  bnd2  9930  kmlem13  10200  brdom3  10565  brdom5  10566  brdom4  10567  fpwwe  10683  canthwelem  10687  pwfseqlem4  10699  ingru  10852  ltweuz  13998  elrest  17473  invfval  17806  isoval  17812  isofn  17822  zeroofn  18042  zerooval  18048  catcval  18153  isacs5lem  18602  isunit  20389  isrhm  20494  rhmfn  20515  rhmval  20516  rhmsubclem1  20701  2idlval  21278  pjfval  21743  psdmul  22187  fctop  23026  cctop  23028  ppttop  23029  epttop  23031  mretopd  23115  toponmre  23116  tgrest  23182  resttopon  23184  restco  23187  ordtbas2  23214  cnrest2  23309  cnpresti  23311  cnprest  23312  cnprest2  23313  cmpsublem  23422  cmpsub  23423  connsuba  23443  1stcrest  23476  subislly  23504  cldllycmp  23518  lly1stc  23519  txrest  23654  basqtop  23734  fbssfi  23860  trfbas2  23866  snfil  23887  fgcl  23901  trfil2  23910  cfinfil  23916  csdfil  23917  supfil  23918  zfbas  23919  fin1aufil  23955  fmfnfmlem3  23979  flimrest  24006  hauspwpwf1  24010  fclsrest  24047  tmdgsum2  24119  tsmsval2  24153  tsmssubm  24166  ustuqtop2  24266  restmetu  24598  isnmhm  24782  icopnfhmeo  24987  iccpnfhmeo  24989  xrhmeo  24990  pi1buni  25086  minveclem3b  25475  uniioombllem2  25631  uniioombllem6  25636  vitali  25661  ellimc2  25926  limcflf  25930  taylfvallem  26413  taylf  26416  tayl0  26417  taylpfval  26420  xrlimcnp  27025  lrrecse  27989  ewlkle  29637  upgrewlkle2  29638  wlk1walk  29671  maprnin  32748  ordtprsval  33878  ordtprsuni  33879  ordtrestNEW  33881  ordtrest2NEWlem  33882  ordtrest2NEW  33883  ordtconnlem1  33884  xrge0iifhmeo  33896  eulerpartgbij  34353  eulerpartlemmf  34356  eulerpart  34363  ballotlemfrc  34507  cvmsss2  35258  cvmcov2  35259  mvrsval  35489  mpstval  35519  mclsind  35554  mthmpps  35566  dfon2lem4  35767  brapply  35919  neibastop1  36341  filnetlem3  36362  weiunfr  36449  bj-restn0  37072  bj-restuni  37079  ptrest  37605  heiborlem3  37799  heibor  37807  polvalN  39887  fnwe2lem2  43039  harval3  43527  superficl  43556  ssficl  43558  trficl  43658  onfrALTlem5  44539  onfrALTlem5VD  44882  fourierdlem48  46109  fourierdlem49  46110  sge0resplit  46361  hoiqssbllem3  46579  rngcvalALTV  48108  rhmsubcALTVlem1  48124  ringcvalALTV  48132