Theorem inex1 5277

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	sepgi 5252	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2754	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3913	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 340	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1852	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 278	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1881	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 234	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3470	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3451   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3904

This theorem is used by:  inex2  5278  inex1g  5279  inuni  5311  onfr  6403  ssimaex  6971  exfo  7106  ofmres  7997  fnwe2lem3  8148  fipwuni  9419  fisn  9420  elfiun  9423  dffi3  9424  marypha1lem  9426  epfrs  9733  tcmin  9741  bnd2  9957  kmlem13  10242  brdom3  10608  brdom5  10609  brdom4  10610  fpwwe  10732  canthwelem  10736  pwfseqlem4  10748  ingru  10901  ltweuz  14105  elrest  17599  invfval  17935  isoval  17941  isofn  17951  zeroofn  18165  zerooval  18171  catcval  18276  isacs5lem  18720  isunit  20604  isrhm  20710  rhmfn  20737  rhmval  20739  rhmsubclem1  20938  2idlval  21545  pjfval  22013  psdmul  22488  fctop  23323  cctop  23325  ppttop  23326  epttop  23328  mretopd  23411  toponmre  23412  tgrest  23478  resttopon  23480  restco  23483  ordtbas2  23510  cnrest2  23605  cnpresti  23607  cnprest  23608  cnprest2  23609  cmpsublem  23718  cmpsub  23719  connsuba  23739  1stcrest  23772  subislly  23801  cldllycmp  23815  lly1stc  23816  txrest  23951  basqtop  24031  fbssfi  24157  trfbas2  24163  snfil  24184  fgcl  24198  trfil2  24207  cfinfil  24213  csdfil  24214  supfil  24215  zfbas  24216  fin1aufil  24252  fmfnfmlem3  24276  flimrest  24303  hauspwpwf1  24307  fclsrest  24344  tmdgsum2  24416  tsmsval2  24450  tsmssubm  24463  ustuqtop2  24562  restmetu  24890  isnmhm  25066  icopnfhmeo  25265  iccpnfhmeo  25267  xrhmeo  25268  pi1buni  25362  minveclem3b  25750  uniioombllem2  25905  uniioombllem6  25910  vitali  25935  ellimc2  26198  limcflf  26202  taylfvallem  26686  taylf  26689  tayl0  26690  taylpfval  26693  xrlimcnp  27297  lrrecse  28329  ewlkle  30187  upgrewlkle2  30188  wlk1walk  30220  maprnin  33324  ordtprsval  34551  ordtprsuni  34552  ordtrestNEW  34554  ordtrest2NEWlem  34555  ordtrest2NEW  34556  ordtconnlem1  34557  xrge0iifhmeo  34569  eulerpartgbij  35005  eulerpartlemmf  35008  eulerpart  35015  ballotlemfrc  35160  weexenwe  35757  cvmsss2  36040  cvmcov2  36041  mvrsval  36271  mpstval  36301  mclsind  36336  mthmpps  36348  dfon2lem4  36549  brapply  36701  neibastop1  37148  filnetlem3  37169  weiunfr  37256  bj-restn0  38012  bj-restuni  38019  ptrest  38539  heiborlem3  38749  heibor  38757  polvalN  40964  harval3  44540  superficl  44569  ssficl  44571  trficl  44670  onfrALTlem5  45526  onfrALTlem5VD  45868  fourierdlem48  47165  fourierdlem49  47166  sge0resplit  47417  hoiqssbllem3  47635  rngcvalALTV  49363  rhmsubcALTVlem1  49379  ringcvalALTV  49387  invfn  50139