Theorem inex1 5335

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 5319	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2733	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3992	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1817	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 275	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1846	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 231	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3507	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108  Vcvv 3488   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983

This theorem is referenced by:  inex2  5336  inex1g  5337  inuni  5368  onfr  6434  ssimaex  7007  exfo  7139  ofmres  8025  fipwuni  9495  fisn  9496  elfiun  9499  dffi3  9500  marypha1lem  9502  epfrs  9800  tcmin  9810  bnd2  9962  kmlem13  10232  brdom3  10597  brdom5  10598  brdom4  10599  fpwwe  10715  canthwelem  10719  pwfseqlem4  10731  ingru  10884  ltweuz  14012  elrest  17487  invfval  17820  isoval  17826  isofn  17836  zeroofn  18056  zerooval  18062  catcval  18167  isacs5lem  18615  isunit  20399  isrhm  20504  rhmfn  20525  rhmval  20526  rhmsubclem1  20707  2idlval  21284  pjfval  21749  psdmul  22193  fctop  23032  cctop  23034  ppttop  23035  epttop  23037  mretopd  23121  toponmre  23122  tgrest  23188  resttopon  23190  restco  23193  ordtbas2  23220  cnrest2  23315  cnpresti  23317  cnprest  23318  cnprest2  23319  cmpsublem  23428  cmpsub  23429  connsuba  23449  1stcrest  23482  subislly  23510  cldllycmp  23524  lly1stc  23525  txrest  23660  basqtop  23740  fbssfi  23866  trfbas2  23872  snfil  23893  fgcl  23907  trfil2  23916  cfinfil  23922  csdfil  23923  supfil  23924  zfbas  23925  fin1aufil  23961  fmfnfmlem3  23985  flimrest  24012  hauspwpwf1  24016  fclsrest  24053  tmdgsum2  24125  tsmsval2  24159  tsmssubm  24172  ustuqtop2  24272  restmetu  24604  isnmhm  24788  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  pi1buni  25092  minveclem3b  25481  uniioombllem2  25637  uniioombllem6  25642  vitali  25667  ellimc2  25932  limcflf  25936  taylfvallem  26417  taylf  26420  tayl0  26421  taylpfval  26424  xrlimcnp  27029  lrrecse  27993  ewlkle  29641  upgrewlkle2  29642  wlk1walk  29675  maprnin  32745  ordtprsval  33864  ordtprsuni  33865  ordtrestNEW  33867  ordtrest2NEWlem  33868  ordtrest2NEW  33869  ordtconnlem1  33870  xrge0iifhmeo  33882  eulerpartgbij  34337  eulerpartlemmf  34340  eulerpart  34347  ballotlemfrc  34491  cvmsss2  35242  cvmcov2  35243  mvrsval  35473  mpstval  35503  mclsind  35538  mthmpps  35550  dfon2lem4  35750  brapply  35902  neibastop1  36325  filnetlem3  36346  weiunfr  36433  bj-restn0  37056  bj-restuni  37063  ptrest  37579  heiborlem3  37773  heibor  37781  polvalN  39862  fnwe2lem2  43008  harval3  43500  superficl  43529  ssficl  43531  trficl  43631  onfrALTlem5  44513  onfrALTlem5VD  44856  fourierdlem48  46075  fourierdlem49  46076  sge0resplit  46327  hoiqssbllem3  46545  rngcvalALTV  47988  rhmsubcALTVlem1  48004  ringcvalALTV  48012