Theorem inex1 5258

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 5233	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2729	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3905	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1821	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 275	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1850	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 231	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3448	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3429   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896

This theorem is referenced by:  inex2  5259  inex1g  5260  inuni  5291  onfr  6362  ssimaex  6925  exfo  7057  ofmres  7937  fipwuni  9339  fisn  9340  elfiun  9343  dffi3  9344  marypha1lem  9346  epfrs  9652  tcmin  9660  bnd2  9817  kmlem13  10085  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe  10569  canthwelem  10573  pwfseqlem4  10585  ingru  10738  ltweuz  13923  elrest  17390  invfval  17726  isoval  17732  isofn  17742  zeroofn  17956  zerooval  17962  catcval  18067  isacs5lem  18511  isunit  20353  isrhm  20458  rhmfn  20476  rhmval  20477  rhmsubclem1  20662  2idlval  21249  pjfval  21686  psdmul  22132  fctop  22969  cctop  22971  ppttop  22972  epttop  22974  mretopd  23057  toponmre  23058  tgrest  23124  resttopon  23126  restco  23129  ordtbas2  23156  cnrest2  23251  cnpresti  23253  cnprest  23254  cnprest2  23255  cmpsublem  23364  cmpsub  23365  connsuba  23385  1stcrest  23418  subislly  23446  cldllycmp  23460  lly1stc  23461  txrest  23596  basqtop  23676  fbssfi  23802  trfbas2  23808  snfil  23829  fgcl  23843  trfil2  23852  cfinfil  23858  csdfil  23859  supfil  23860  zfbas  23861  fin1aufil  23897  fmfnfmlem3  23921  flimrest  23948  hauspwpwf1  23952  fclsrest  23989  tmdgsum2  24061  tsmsval2  24095  tsmssubm  24108  ustuqtop2  24207  restmetu  24535  isnmhm  24711  icopnfhmeo  24910  iccpnfhmeo  24912  xrhmeo  24913  pi1buni  25007  minveclem3b  25395  uniioombllem2  25550  uniioombllem6  25555  vitali  25580  ellimc2  25844  limcflf  25848  taylfvallem  26323  taylf  26326  tayl0  26327  taylpfval  26330  xrlimcnp  26932  lrrecse  27934  ewlkle  29674  upgrewlkle2  29675  wlk1walk  29707  maprnin  32804  ordtprsval  34062  ordtprsuni  34063  ordtrestNEW  34065  ordtrest2NEWlem  34066  ordtrest2NEW  34067  ordtconnlem1  34068  xrge0iifhmeo  34080  eulerpartgbij  34516  eulerpartlemmf  34519  eulerpart  34526  ballotlemfrc  34671  cvmsss2  35456  cvmcov2  35457  mvrsval  35687  mpstval  35717  mclsind  35752  mthmpps  35764  dfon2lem4  35966  brapply  36118  neibastop1  36541  filnetlem3  36562  weiunfr  36649  bj-restn0  37402  bj-restuni  37409  ptrest  37940  heiborlem3  38134  heibor  38142  polvalN  40351  fnwe2lem2  43479  harval3  43965  superficl  43994  ssficl  43996  trficl  44096  onfrALTlem5  44969  onfrALTlem5VD  45311  fourierdlem48  46582  fourierdlem49  46583  sge0resplit  46834  hoiqssbllem3  47052  rngcvalALTV  48741  rhmsubcALTVlem1  48757  ringcvalALTV  48765  invfn  49505