Theorem inex1 4832

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 4816	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2645	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3829	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 326	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1787	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 264	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1814	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 221	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3241	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 196   ∧ wa 383  ∀wal 1521   = wceq 1523  ∃wex 1744   ∈ wcel 2030  Vcvv 3231   ∩ cin 3606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614

This theorem is referenced by:  inex2  4833  inex1g  4834  inuni  4856  predasetex  5733  onfr  5801  ssimaex  6302  exfo  6417  ofmres  7206  fipwuni  8373  fisn  8374  elfiun  8377  dffi3  8378  marypha1lem  8380  epfrs  8645  tcmin  8655  bnd2  8794  kmlem13  9022  brdom3  9388  brdom5  9389  brdom4  9390  fpwwe  9506  canthwelem  9510  pwfseqlem4  9522  ingru  9675  ltweuz  12800  elrest  16135  invfval  16466  isoval  16472  isofn  16482  zerooval  16696  catcval  16793  isacs5lem  17216  isunit  18703  isrhm  18769  2idlval  19281  pjfval  20098  fctop  20856  cctop  20858  ppttop  20859  epttop  20861  mretopd  20944  toponmre  20945  tgrest  21011  resttopon  21013  restco  21016  ordtbas2  21043  cnrest2  21138  cnpresti  21140  cnprest  21141  cnprest2  21142  cmpsublem  21250  cmpsub  21251  connsuba  21271  1stcrest  21304  subislly  21332  cldllycmp  21346  lly1stc  21347  txrest  21482  basqtop  21562  fbssfi  21688  trfbas2  21694  snfil  21715  fgcl  21729  trfil2  21738  cfinfil  21744  csdfil  21745  supfil  21746  zfbas  21747  fin1aufil  21783  fmfnfmlem3  21807  flimrest  21834  hauspwpwf1  21838  fclsrest  21875  tmdgsum2  21947  tsmsval2  21980  tsmssubm  21993  ustuqtop2  22093  metustfbas  22409  restmetu  22422  isnmhm  22597  icopnfhmeo  22789  iccpnfhmeo  22791  xrhmeo  22792  pi1buni  22886  minveclem3b  23245  uniioombllem2  23397  uniioombllem6  23402  vitali  23427  ellimc2  23686  limcflf  23690  taylfvallem  24157  taylf  24160  tayl0  24161  taylpfval  24164  xrlimcnp  24740  ewlkle  26557  upgrewlkle2  26558  wlk1walk  26591  maprnin  29634  ordtprsval  30092  ordtprsuni  30093  ordtrestNEW  30095  ordtrest2NEWlem  30096  ordtrest2NEW  30097  ordtconnlem1  30098  xrge0iifhmeo  30110  eulerpartgbij  30562  eulerpartlemmf  30565  eulerpart  30572  ballotlemfrc  30716  cvmsss2  31382  cvmcov2  31383  mvrsval  31528  mpstval  31558  mclsind  31593  mthmpps  31605  dfon2lem4  31815  brapply  32170  neibastop1  32479  filnetlem3  32500  bj-restn0  33168  bj-restuni  33175  ptrest  33538  heiborlem3  33742  heibor  33750  polvalN  35509  fnwe2lem2  37938  superficl  38189  ssficl  38191  trficl  38278  onfrALTlem5  39074  onfrALTlem5VD  39435  fourierdlem48  40689  fourierdlem49  40690  sge0resplit  40941  hoiqssbllem3  41159  rhmfn  42243  rhmval  42244  rngcvalALTV  42286  ringcvalALTV  42332  rhmsubclem1  42411  rhmsubcALTVlem1  42429