Theorem inex1 5275

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 5256	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2723	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3933	. . . . . . 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 3469	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

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

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 2702  ax-sep 5254

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924

This theorem is referenced by:  inex2  5276  inex1g  5277  inuni  5308  onfr  6374  ssimaex  6949  exfo  7080  ofmres  7966  fipwuni  9384  fisn  9385  elfiun  9388  dffi3  9389  marypha1lem  9391  epfrs  9691  tcmin  9701  bnd2  9853  kmlem13  10123  brdom3  10488  brdom5  10489  brdom4  10490  fpwwe  10606  canthwelem  10610  pwfseqlem4  10622  ingru  10775  ltweuz  13933  elrest  17397  invfval  17728  isoval  17734  isofn  17744  zeroofn  17958  zerooval  17964  catcval  18069  isacs5lem  18511  isunit  20289  isrhm  20394  rhmfn  20415  rhmval  20416  rhmsubclem1  20601  2idlval  21168  pjfval  21622  psdmul  22060  fctop  22898  cctop  22900  ppttop  22901  epttop  22903  mretopd  22986  toponmre  22987  tgrest  23053  resttopon  23055  restco  23058  ordtbas2  23085  cnrest2  23180  cnpresti  23182  cnprest  23183  cnprest2  23184  cmpsublem  23293  cmpsub  23294  connsuba  23314  1stcrest  23347  subislly  23375  cldllycmp  23389  lly1stc  23390  txrest  23525  basqtop  23605  fbssfi  23731  trfbas2  23737  snfil  23758  fgcl  23772  trfil2  23781  cfinfil  23787  csdfil  23788  supfil  23789  zfbas  23790  fin1aufil  23826  fmfnfmlem3  23850  flimrest  23877  hauspwpwf1  23881  fclsrest  23918  tmdgsum2  23990  tsmsval2  24024  tsmssubm  24037  ustuqtop2  24137  restmetu  24465  isnmhm  24641  icopnfhmeo  24848  iccpnfhmeo  24850  xrhmeo  24851  pi1buni  24947  minveclem3b  25335  uniioombllem2  25491  uniioombllem6  25496  vitali  25521  ellimc2  25785  limcflf  25789  taylfvallem  26272  taylf  26275  tayl0  26276  taylpfval  26279  xrlimcnp  26885  lrrecse  27856  ewlkle  29540  upgrewlkle2  29541  wlk1walk  29574  maprnin  32661  ordtprsval  33915  ordtprsuni  33916  ordtrestNEW  33918  ordtrest2NEWlem  33919  ordtrest2NEW  33920  ordtconnlem1  33921  xrge0iifhmeo  33933  eulerpartgbij  34370  eulerpartlemmf  34373  eulerpart  34380  ballotlemfrc  34525  cvmsss2  35268  cvmcov2  35269  mvrsval  35499  mpstval  35529  mclsind  35564  mthmpps  35576  dfon2lem4  35781  brapply  35933  neibastop1  36354  filnetlem3  36375  weiunfr  36462  bj-restn0  37085  bj-restuni  37092  ptrest  37620  heiborlem3  37814  heibor  37822  polvalN  39906  fnwe2lem2  43047  harval3  43534  superficl  43563  ssficl  43565  trficl  43665  onfrALTlem5  44539  onfrALTlem5VD  44881  fourierdlem48  46159  fourierdlem49  46160  sge0resplit  46411  hoiqssbllem3  46629  rngcvalALTV  48257  rhmsubcALTVlem1  48273  ringcvalALTV  48281  invfn  49023