Theorem inex1 5236

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 5220	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2731	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3899	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1823	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 274	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1851	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 230	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3438	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 205   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108  Vcvv 3422   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890

This theorem is referenced by:  inex2  5237  inex1g  5238  inuni  5262  onfr  6290  ssimaex  6835  exfo  6963  ofmres  7800  fipwuni  9115  fisn  9116  elfiun  9119  dffi3  9120  marypha1lem  9122  epfrs  9420  tcmin  9430  bnd2  9582  kmlem13  9849  brdom3  10215  brdom5  10216  brdom4  10217  fpwwe  10333  canthwelem  10337  pwfseqlem4  10349  ingru  10502  ltweuz  13609  elrest  17055  invfval  17388  isoval  17394  isofn  17404  zeroofn  17620  zerooval  17626  catcval  17731  isacs5lem  18178  isunit  19814  isrhm  19880  2idlval  20417  pjfval  20823  fctop  22062  cctop  22064  ppttop  22065  epttop  22067  mretopd  22151  toponmre  22152  tgrest  22218  resttopon  22220  restco  22223  ordtbas2  22250  cnrest2  22345  cnpresti  22347  cnprest  22348  cnprest2  22349  cmpsublem  22458  cmpsub  22459  connsuba  22479  1stcrest  22512  subislly  22540  cldllycmp  22554  lly1stc  22555  txrest  22690  basqtop  22770  fbssfi  22896  trfbas2  22902  snfil  22923  fgcl  22937  trfil2  22946  cfinfil  22952  csdfil  22953  supfil  22954  zfbas  22955  fin1aufil  22991  fmfnfmlem3  23015  flimrest  23042  hauspwpwf1  23046  fclsrest  23083  tmdgsum2  23155  tsmsval2  23189  tsmssubm  23202  ustuqtop2  23302  restmetu  23632  isnmhm  23816  icopnfhmeo  24012  iccpnfhmeo  24014  xrhmeo  24015  pi1buni  24109  minveclem3b  24497  uniioombllem2  24652  uniioombllem6  24657  vitali  24682  ellimc2  24946  limcflf  24950  taylfvallem  25422  taylf  25425  tayl0  25426  taylpfval  25429  xrlimcnp  26023  ewlkle  27875  upgrewlkle2  27876  wlk1walk  27908  maprnin  30968  ordtprsval  31770  ordtprsuni  31771  ordtrestNEW  31773  ordtrest2NEWlem  31774  ordtrest2NEW  31775  ordtconnlem1  31776  xrge0iifhmeo  31788  eulerpartgbij  32239  eulerpartlemmf  32242  eulerpart  32249  ballotlemfrc  32393  cvmsss2  33136  cvmcov2  33137  mvrsval  33367  mpstval  33397  mclsind  33432  mthmpps  33444  dfon2lem4  33668  lrrecse  34026  brapply  34167  neibastop1  34475  filnetlem3  34496  bj-restn0  35188  bj-restuni  35195  ptrest  35703  heiborlem3  35898  heibor  35906  polvalN  37846  fnwe2lem2  40792  harval3  41041  superficl  41063  ssficl  41065  trficl  41166  onfrALTlem5  42051  onfrALTlem5VD  42394  fourierdlem48  43585  fourierdlem49  43586  sge0resplit  43834  hoiqssbllem3  44052  rhmfn  45364  rhmval  45365  rngcvalALTV  45407  ringcvalALTV  45453  rhmsubclem1  45532  rhmsubcALTVlem1  45550