Theorem inex1 5267

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 5248	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2722	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3927	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1819	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 275	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1848	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 231	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3463	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3444   ∩ cin 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-in 3918

This theorem is referenced by:  inex2  5268  inex1g  5269  inuni  5300  onfr  6359  ssimaex  6928  exfo  7059  ofmres  7942  fipwuni  9353  fisn  9354  elfiun  9357  dffi3  9358  marypha1lem  9360  epfrs  9660  tcmin  9670  bnd2  9822  kmlem13  10092  brdom3  10457  brdom5  10458  brdom4  10459  fpwwe  10575  canthwelem  10579  pwfseqlem4  10591  ingru  10744  ltweuz  13902  elrest  17366  invfval  17701  isoval  17707  isofn  17717  zeroofn  17931  zerooval  17937  catcval  18042  isacs5lem  18486  isunit  20293  isrhm  20398  rhmfn  20419  rhmval  20420  rhmsubclem1  20605  2idlval  21193  pjfval  21648  psdmul  22086  fctop  22924  cctop  22926  ppttop  22927  epttop  22929  mretopd  23012  toponmre  23013  tgrest  23079  resttopon  23081  restco  23084  ordtbas2  23111  cnrest2  23206  cnpresti  23208  cnprest  23209  cnprest2  23210  cmpsublem  23319  cmpsub  23320  connsuba  23340  1stcrest  23373  subislly  23401  cldllycmp  23415  lly1stc  23416  txrest  23551  basqtop  23631  fbssfi  23757  trfbas2  23763  snfil  23784  fgcl  23798  trfil2  23807  cfinfil  23813  csdfil  23814  supfil  23815  zfbas  23816  fin1aufil  23852  fmfnfmlem3  23876  flimrest  23903  hauspwpwf1  23907  fclsrest  23944  tmdgsum2  24016  tsmsval2  24050  tsmssubm  24063  ustuqtop2  24163  restmetu  24491  isnmhm  24667  icopnfhmeo  24874  iccpnfhmeo  24876  xrhmeo  24877  pi1buni  24973  minveclem3b  25361  uniioombllem2  25517  uniioombllem6  25522  vitali  25547  ellimc2  25811  limcflf  25815  taylfvallem  26298  taylf  26301  tayl0  26302  taylpfval  26305  xrlimcnp  26911  lrrecse  27889  ewlkle  29586  upgrewlkle2  29587  wlk1walk  29619  maprnin  32704  ordtprsval  33901  ordtprsuni  33902  ordtrestNEW  33904  ordtrest2NEWlem  33905  ordtrest2NEW  33906  ordtconnlem1  33907  xrge0iifhmeo  33919  eulerpartgbij  34356  eulerpartlemmf  34359  eulerpart  34366  ballotlemfrc  34511  cvmsss2  35254  cvmcov2  35255  mvrsval  35485  mpstval  35515  mclsind  35550  mthmpps  35562  dfon2lem4  35767  brapply  35919  neibastop1  36340  filnetlem3  36361  weiunfr  36448  bj-restn0  37071  bj-restuni  37078  ptrest  37606  heiborlem3  37800  heibor  37808  polvalN  39892  fnwe2lem2  43033  harval3  43520  superficl  43549  ssficl  43551  trficl  43651  onfrALTlem5  44525  onfrALTlem5VD  44867  fourierdlem48  46145  fourierdlem49  46146  sge0resplit  46397  hoiqssbllem3  46615  rngcvalALTV  48246  rhmsubcALTVlem1  48262  ringcvalALTV  48270  invfn  49012