Theorem inex1 5262

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2113  Vcvv 3440   ∩ cin 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908

This theorem is referenced by:  inex2  5263  inex1g  5264  inuni  5295  onfr  6356  ssimaex  6919  exfo  7050  ofmres  7928  fipwuni  9329  fisn  9330  elfiun  9333  dffi3  9334  marypha1lem  9336  epfrs  9640  tcmin  9648  bnd2  9805  kmlem13  10073  brdom3  10438  brdom5  10439  brdom4  10440  fpwwe  10557  canthwelem  10561  pwfseqlem4  10573  ingru  10726  ltweuz  13884  elrest  17347  invfval  17683  isoval  17689  isofn  17699  zeroofn  17913  zerooval  17919  catcval  18024  isacs5lem  18468  isunit  20309  isrhm  20414  rhmfn  20432  rhmval  20433  rhmsubclem1  20618  2idlval  21206  pjfval  21661  psdmul  22109  fctop  22948  cctop  22950  ppttop  22951  epttop  22953  mretopd  23036  toponmre  23037  tgrest  23103  resttopon  23105  restco  23108  ordtbas2  23135  cnrest2  23230  cnpresti  23232  cnprest  23233  cnprest2  23234  cmpsublem  23343  cmpsub  23344  connsuba  23364  1stcrest  23397  subislly  23425  cldllycmp  23439  lly1stc  23440  txrest  23575  basqtop  23655  fbssfi  23781  trfbas2  23787  snfil  23808  fgcl  23822  trfil2  23831  cfinfil  23837  csdfil  23838  supfil  23839  zfbas  23840  fin1aufil  23876  fmfnfmlem3  23900  flimrest  23927  hauspwpwf1  23931  fclsrest  23968  tmdgsum2  24040  tsmsval2  24074  tsmssubm  24087  ustuqtop2  24186  restmetu  24514  isnmhm  24690  icopnfhmeo  24897  iccpnfhmeo  24899  xrhmeo  24900  pi1buni  24996  minveclem3b  25384  uniioombllem2  25540  uniioombllem6  25545  vitali  25570  ellimc2  25834  limcflf  25838  taylfvallem  26321  taylf  26324  tayl0  26325  taylpfval  26328  xrlimcnp  26934  lrrecse  27938  ewlkle  29679  upgrewlkle2  29680  wlk1walk  29712  maprnin  32810  ordtprsval  34075  ordtprsuni  34076  ordtrestNEW  34078  ordtrest2NEWlem  34079  ordtrest2NEW  34080  ordtconnlem1  34081  xrge0iifhmeo  34093  eulerpartgbij  34529  eulerpartlemmf  34532  eulerpart  34539  ballotlemfrc  34684  cvmsss2  35468  cvmcov2  35469  mvrsval  35699  mpstval  35729  mclsind  35764  mthmpps  35776  dfon2lem4  35978  brapply  36130  neibastop1  36553  filnetlem3  36574  weiunfr  36661  bj-restn0  37295  bj-restuni  37302  ptrest  37820  heiborlem3  38014  heibor  38022  polvalN  40175  fnwe2lem2  43303  harval3  43789  superficl  43818  ssficl  43820  trficl  43920  onfrALTlem5  44793  onfrALTlem5VD  45135  fourierdlem48  46408  fourierdlem49  46409  sge0resplit  46660  hoiqssbllem3  46878  rngcvalALTV  48521  rhmsubcALTVlem1  48537  ringcvalALTV  48545  invfn  49285