Theorem inex1 5280

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  Vcvv 3450   ∩ 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 2732  ax-sep 5251

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906

This theorem is used by:  inex2  5281  inex1g  5282  inuni  5314  onfr  6397  ssimaex  6964  exfo  7099  ofmres  7982  fipwuni  9397  fisn  9398  elfiun  9401  dffi3  9402  marypha1lem  9404  epfrs  9711  tcmin  9719  bnd2  9896  kmlem13  10166  brdom3  10532  brdom5  10533  brdom4  10534  fpwwe  10656  canthwelem  10660  pwfseqlem4  10672  ingru  10825  ltweuz  14026  elrest  17513  invfval  17849  isoval  17855  isofn  17865  zeroofn  18079  zerooval  18085  catcval  18190  isacs5lem  18634  isunit  20515  isrhm  20621  rhmfn  20648  rhmval  20650  rhmsubclem1  20848  2idlval  21454  pjfval  21920  psdmul  22395  fctop  23230  cctop  23232  ppttop  23233  epttop  23235  mretopd  23318  toponmre  23319  tgrest  23385  resttopon  23387  restco  23390  ordtbas2  23417  cnrest2  23512  cnpresti  23514  cnprest  23515  cnprest2  23516  cmpsublem  23625  cmpsub  23626  connsuba  23646  1stcrest  23679  subislly  23708  cldllycmp  23722  lly1stc  23723  txrest  23858  basqtop  23938  fbssfi  24064  trfbas2  24070  snfil  24091  fgcl  24105  trfil2  24114  cfinfil  24120  csdfil  24121  supfil  24122  zfbas  24123  fin1aufil  24159  fmfnfmlem3  24183  flimrest  24210  hauspwpwf1  24214  fclsrest  24251  tmdgsum2  24323  tsmsval2  24357  tsmssubm  24370  ustuqtop2  24469  restmetu  24797  isnmhm  24973  icopnfhmeo  25172  iccpnfhmeo  25174  xrhmeo  25175  pi1buni  25269  minveclem3b  25657  uniioombllem2  25812  uniioombllem6  25817  vitali  25842  ellimc2  26105  limcflf  26109  taylfvallem  26595  taylf  26598  tayl0  26599  taylpfval  26602  xrlimcnp  27206  lrrecse  28208  ewlkle  30066  upgrewlkle2  30067  wlk1walk  30099  maprnin  33203  ordtprsval  34429  ordtprsuni  34430  ordtrestNEW  34432  ordtrest2NEWlem  34433  ordtrest2NEW  34434  ordtconnlem1  34435  xrge0iifhmeo  34447  eulerpartgbij  34884  eulerpartlemmf  34887  eulerpart  34894  ballotlemfrc  35039  cvmsss2  35854  cvmcov2  35855  mvrsval  36085  mpstval  36115  mclsind  36150  mthmpps  36162  dfon2lem4  36364  brapply  36516  neibastop1  36979  filnetlem3  37000  weiunfr  37087  bj-restn0  37841  bj-restuni  37848  ptrest  38369  heiborlem3  38564  heibor  38572  polvalN  40779  fnwe2lem2  43893  harval3  44379  superficl  44408  ssficl  44410  trficl  44510  onfrALTlem5  45366  onfrALTlem5VD  45708  fourierdlem48  46983  fourierdlem49  46984  sge0resplit  47235  hoiqssbllem3  47453  rngcvalALTV  49181  rhmsubcALTVlem1  49197  ringcvalALTV  49205  invfn  49957