Theorem inex1 5317

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 5301	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2721	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3963	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1814	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 275	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1843	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 230	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3488	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 205   ∧ wa 395  ∀wal 1532   = wceq 1534  ∃wex 1774   ∈ wcel 2099  Vcvv 3471   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5299

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-in 3954

This theorem is referenced by:  inex2  5318  inex1g  5319  inuni  5345  onfr  6408  ssimaex  6983  exfo  7115  ofmres  7988  fipwuni  9449  fisn  9450  elfiun  9453  dffi3  9454  marypha1lem  9456  epfrs  9754  tcmin  9764  bnd2  9916  kmlem13  10185  brdom3  10551  brdom5  10552  brdom4  10553  fpwwe  10669  canthwelem  10673  pwfseqlem4  10685  ingru  10838  ltweuz  13958  elrest  17408  invfval  17741  isoval  17747  isofn  17757  zeroofn  17977  zerooval  17983  catcval  18088  isacs5lem  18536  isunit  20311  isrhm  20416  rhmfn  20437  rhmval  20438  rhmsubclem1  20617  2idlval  21144  pjfval  21639  psdmul  22089  fctop  22906  cctop  22908  ppttop  22909  epttop  22911  mretopd  22995  toponmre  22996  tgrest  23062  resttopon  23064  restco  23067  ordtbas2  23094  cnrest2  23189  cnpresti  23191  cnprest  23192  cnprest2  23193  cmpsublem  23302  cmpsub  23303  connsuba  23323  1stcrest  23356  subislly  23384  cldllycmp  23398  lly1stc  23399  txrest  23534  basqtop  23614  fbssfi  23740  trfbas2  23746  snfil  23767  fgcl  23781  trfil2  23790  cfinfil  23796  csdfil  23797  supfil  23798  zfbas  23799  fin1aufil  23835  fmfnfmlem3  23859  flimrest  23886  hauspwpwf1  23890  fclsrest  23927  tmdgsum2  23999  tsmsval2  24033  tsmssubm  24046  ustuqtop2  24146  restmetu  24478  isnmhm  24662  icopnfhmeo  24867  iccpnfhmeo  24869  xrhmeo  24870  pi1buni  24966  minveclem3b  25355  uniioombllem2  25511  uniioombllem6  25516  vitali  25541  ellimc2  25805  limcflf  25809  taylfvallem  26291  taylf  26294  tayl0  26295  taylpfval  26298  xrlimcnp  26899  lrrecse  27858  ewlkle  29418  upgrewlkle2  29419  wlk1walk  29452  maprnin  32513  ordtprsval  33519  ordtprsuni  33520  ordtrestNEW  33522  ordtrest2NEWlem  33523  ordtrest2NEW  33524  ordtconnlem1  33525  xrge0iifhmeo  33537  eulerpartgbij  33992  eulerpartlemmf  33995  eulerpart  34002  ballotlemfrc  34146  cvmsss2  34884  cvmcov2  34885  mvrsval  35115  mpstval  35145  mclsind  35180  mthmpps  35192  dfon2lem4  35382  brapply  35534  neibastop1  35843  filnetlem3  35864  bj-restn0  36569  bj-restuni  36576  ptrest  37092  heiborlem3  37286  heibor  37294  polvalN  39378  fnwe2lem2  42475  harval3  42968  superficl  42997  ssficl  42999  trficl  43099  onfrALTlem5  43981  onfrALTlem5VD  44324  fourierdlem48  45542  fourierdlem49  45543  sge0resplit  45794  hoiqssbllem3  46012  rngcvalALTV  47327  rhmsubcALTVlem1  47343  ringcvalALTV  47351