Theorem inex1 5317

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 5301	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2721	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3963	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1814	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 275	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1843	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 230	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3488	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 205   ∧ wa 395  ∀wal 1532   = wceq 1534  ∃wex 1774   ∈ wcel 2099  Vcvv 3471   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954

This theorem is referenced by:  inex2  5318  inex1g  5319  inuni  5345  onfr  6408  ssimaex  6983  exfo  7115  ofmres  7988  fipwuni  9450  fisn  9451  elfiun  9454  dffi3  9455  marypha1lem  9457  epfrs  9755  tcmin  9765  bnd2  9917  kmlem13  10186  brdom3  10552  brdom5  10553  brdom4  10554  fpwwe  10670  canthwelem  10674  pwfseqlem4  10686  ingru  10839  ltweuz  13959  elrest  17409  invfval  17742  isoval  17748  isofn  17758  zeroofn  17978  zerooval  17984  catcval  18089  isacs5lem  18537  isunit  20312  isrhm  20417  rhmfn  20438  rhmval  20439  rhmsubclem1  20618  2idlval  21145  pjfval  21640  psdmul  22090  fctop  22920  cctop  22922  ppttop  22923  epttop  22925  mretopd  23009  toponmre  23010  tgrest  23076  resttopon  23078  restco  23081  ordtbas2  23108  cnrest2  23203  cnpresti  23205  cnprest  23206  cnprest2  23207  cmpsublem  23316  cmpsub  23317  connsuba  23337  1stcrest  23370  subislly  23398  cldllycmp  23412  lly1stc  23413  txrest  23548  basqtop  23628  fbssfi  23754  trfbas2  23760  snfil  23781  fgcl  23795  trfil2  23804  cfinfil  23810  csdfil  23811  supfil  23812  zfbas  23813  fin1aufil  23849  fmfnfmlem3  23873  flimrest  23900  hauspwpwf1  23904  fclsrest  23941  tmdgsum2  24013  tsmsval2  24047  tsmssubm  24060  ustuqtop2  24160  restmetu  24492  isnmhm  24676  icopnfhmeo  24881  iccpnfhmeo  24883  xrhmeo  24884  pi1buni  24980  minveclem3b  25369  uniioombllem2  25525  uniioombllem6  25530  vitali  25555  ellimc2  25819  limcflf  25823  taylfvallem  26305  taylf  26308  tayl0  26309  taylpfval  26312  xrlimcnp  26913  lrrecse  27872  ewlkle  29432  upgrewlkle2  29433  wlk1walk  29466  maprnin  32526  ordtprsval  33519  ordtprsuni  33520  ordtrestNEW  33522  ordtrest2NEWlem  33523  ordtrest2NEW  33524  ordtconnlem1  33525  xrge0iifhmeo  33537  eulerpartgbij  33992  eulerpartlemmf  33995  eulerpart  34002  ballotlemfrc  34146  cvmsss2  34884  cvmcov2  34885  mvrsval  35115  mpstval  35145  mclsind  35180  mthmpps  35192  dfon2lem4  35382  brapply  35534  neibastop1  35843  filnetlem3  35864  bj-restn0  36569  bj-restuni  36576  ptrest  37092  heiborlem3  37286  heibor  37294  polvalN  39378  fnwe2lem2  42475  harval3  42968  superficl  42997  ssficl  42999  trficl  43099  onfrALTlem5  43981  onfrALTlem5VD  44324  fourierdlem48  45542  fourierdlem49  45543  sge0resplit  45794  hoiqssbllem3  46012  rngcvalALTV  47327  rhmsubcALTVlem1  47343  ringcvalALTV  47351