Theorem inex1 5264

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 5245	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2730	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3919	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1821	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 275	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1850	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 231	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3461	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3442   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910

This theorem is referenced by:  inex2  5265  inex1g  5266  inuni  5297  onfr  6364  ssimaex  6927  exfo  7059  ofmres  7938  fipwuni  9341  fisn  9342  elfiun  9345  dffi3  9346  marypha1lem  9348  epfrs  9652  tcmin  9660  bnd2  9817  kmlem13  10085  brdom3  10450  brdom5  10451  brdom4  10452  fpwwe  10569  canthwelem  10573  pwfseqlem4  10585  ingru  10738  ltweuz  13896  elrest  17359  invfval  17695  isoval  17701  isofn  17711  zeroofn  17925  zerooval  17931  catcval  18036  isacs5lem  18480  isunit  20321  isrhm  20426  rhmfn  20444  rhmval  20445  rhmsubclem1  20630  2idlval  21218  pjfval  21673  psdmul  22121  fctop  22960  cctop  22962  ppttop  22963  epttop  22965  mretopd  23048  toponmre  23049  tgrest  23115  resttopon  23117  restco  23120  ordtbas2  23147  cnrest2  23242  cnpresti  23244  cnprest  23245  cnprest2  23246  cmpsublem  23355  cmpsub  23356  connsuba  23376  1stcrest  23409  subislly  23437  cldllycmp  23451  lly1stc  23452  txrest  23587  basqtop  23667  fbssfi  23793  trfbas2  23799  snfil  23820  fgcl  23834  trfil2  23843  cfinfil  23849  csdfil  23850  supfil  23851  zfbas  23852  fin1aufil  23888  fmfnfmlem3  23912  flimrest  23939  hauspwpwf1  23943  fclsrest  23980  tmdgsum2  24052  tsmsval2  24086  tsmssubm  24099  ustuqtop2  24198  restmetu  24526  isnmhm  24702  icopnfhmeo  24909  iccpnfhmeo  24911  xrhmeo  24912  pi1buni  25008  minveclem3b  25396  uniioombllem2  25552  uniioombllem6  25557  vitali  25582  ellimc2  25846  limcflf  25850  taylfvallem  26333  taylf  26336  tayl0  26337  taylpfval  26340  xrlimcnp  26946  lrrecse  27950  ewlkle  29691  upgrewlkle2  29692  wlk1walk  29724  maprnin  32821  ordtprsval  34096  ordtprsuni  34097  ordtrestNEW  34099  ordtrest2NEWlem  34100  ordtrest2NEW  34101  ordtconnlem1  34102  xrge0iifhmeo  34114  eulerpartgbij  34550  eulerpartlemmf  34553  eulerpart  34560  ballotlemfrc  34705  cvmsss2  35490  cvmcov2  35491  mvrsval  35721  mpstval  35751  mclsind  35786  mthmpps  35798  dfon2lem4  36000  brapply  36152  neibastop1  36575  filnetlem3  36596  weiunfr  36683  bj-restn0  37343  bj-restuni  37350  ptrest  37870  heiborlem3  38064  heibor  38072  polvalN  40281  fnwe2lem2  43408  harval3  43894  superficl  43923  ssficl  43925  trficl  44025  onfrALTlem5  44898  onfrALTlem5VD  45240  fourierdlem48  46512  fourierdlem49  46513  sge0resplit  46764  hoiqssbllem3  46982  rngcvalALTV  48625  rhmsubcALTVlem1  48641  ringcvalALTV  48649  invfn  49389