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 5298	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2730	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3967	. . . . . . 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 3499	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3480   ∩ cin 3950

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958

This theorem is referenced by:  inex2  5318  inex1g  5319  inuni  5350  onfr  6423  ssimaex  6994  exfo  7125  ofmres  8009  fipwuni  9466  fisn  9467  elfiun  9470  dffi3  9471  marypha1lem  9473  epfrs  9771  tcmin  9781  bnd2  9933  kmlem13  10203  brdom3  10568  brdom5  10569  brdom4  10570  fpwwe  10686  canthwelem  10690  pwfseqlem4  10702  ingru  10855  ltweuz  14002  elrest  17472  invfval  17803  isoval  17809  isofn  17819  zeroofn  18034  zerooval  18040  catcval  18145  isacs5lem  18590  isunit  20373  isrhm  20478  rhmfn  20499  rhmval  20500  rhmsubclem1  20685  2idlval  21261  pjfval  21726  psdmul  22170  fctop  23011  cctop  23013  ppttop  23014  epttop  23016  mretopd  23100  toponmre  23101  tgrest  23167  resttopon  23169  restco  23172  ordtbas2  23199  cnrest2  23294  cnpresti  23296  cnprest  23297  cnprest2  23298  cmpsublem  23407  cmpsub  23408  connsuba  23428  1stcrest  23461  subislly  23489  cldllycmp  23503  lly1stc  23504  txrest  23639  basqtop  23719  fbssfi  23845  trfbas2  23851  snfil  23872  fgcl  23886  trfil2  23895  cfinfil  23901  csdfil  23902  supfil  23903  zfbas  23904  fin1aufil  23940  fmfnfmlem3  23964  flimrest  23991  hauspwpwf1  23995  fclsrest  24032  tmdgsum2  24104  tsmsval2  24138  tsmssubm  24151  ustuqtop2  24251  restmetu  24583  isnmhm  24767  icopnfhmeo  24974  iccpnfhmeo  24976  xrhmeo  24977  pi1buni  25073  minveclem3b  25462  uniioombllem2  25618  uniioombllem6  25623  vitali  25648  ellimc2  25912  limcflf  25916  taylfvallem  26399  taylf  26402  tayl0  26403  taylpfval  26406  xrlimcnp  27011  lrrecse  27975  ewlkle  29623  upgrewlkle2  29624  wlk1walk  29657  maprnin  32742  ordtprsval  33917  ordtprsuni  33918  ordtrestNEW  33920  ordtrest2NEWlem  33921  ordtrest2NEW  33922  ordtconnlem1  33923  xrge0iifhmeo  33935  eulerpartgbij  34374  eulerpartlemmf  34377  eulerpart  34384  ballotlemfrc  34529  cvmsss2  35279  cvmcov2  35280  mvrsval  35510  mpstval  35540  mclsind  35575  mthmpps  35587  dfon2lem4  35787  brapply  35939  neibastop1  36360  filnetlem3  36381  weiunfr  36468  bj-restn0  37091  bj-restuni  37098  ptrest  37626  heiborlem3  37820  heibor  37828  polvalN  39907  fnwe2lem2  43063  harval3  43551  superficl  43580  ssficl  43582  trficl  43682  onfrALTlem5  44562  onfrALTlem5VD  44905  fourierdlem48  46169  fourierdlem49  46170  sge0resplit  46421  hoiqssbllem3  46639  rngcvalALTV  48181  rhmsubcALTVlem1  48197  ringcvalALTV  48205