Theorem inex1 5256

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3436   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-in 3910

This theorem is referenced by:  inex2  5257  inex1g  5258  inuni  5289  onfr  6346  ssimaex  6908  exfo  7039  ofmres  7919  fipwuni  9316  fisn  9317  elfiun  9320  dffi3  9321  marypha1lem  9323  epfrs  9627  tcmin  9637  bnd2  9789  kmlem13  10057  brdom3  10422  brdom5  10423  brdom4  10424  fpwwe  10540  canthwelem  10544  pwfseqlem4  10556  ingru  10709  ltweuz  13868  elrest  17331  invfval  17666  isoval  17672  isofn  17682  zeroofn  17896  zerooval  17902  catcval  18007  isacs5lem  18451  isunit  20258  isrhm  20363  rhmfn  20384  rhmval  20385  rhmsubclem1  20570  2idlval  21158  pjfval  21613  psdmul  22051  fctop  22889  cctop  22891  ppttop  22892  epttop  22894  mretopd  22977  toponmre  22978  tgrest  23044  resttopon  23046  restco  23049  ordtbas2  23076  cnrest2  23171  cnpresti  23173  cnprest  23174  cnprest2  23175  cmpsublem  23284  cmpsub  23285  connsuba  23305  1stcrest  23338  subislly  23366  cldllycmp  23380  lly1stc  23381  txrest  23516  basqtop  23596  fbssfi  23722  trfbas2  23728  snfil  23749  fgcl  23763  trfil2  23772  cfinfil  23778  csdfil  23779  supfil  23780  zfbas  23781  fin1aufil  23817  fmfnfmlem3  23841  flimrest  23868  hauspwpwf1  23872  fclsrest  23909  tmdgsum2  23981  tsmsval2  24015  tsmssubm  24028  ustuqtop2  24128  restmetu  24456  isnmhm  24632  icopnfhmeo  24839  iccpnfhmeo  24841  xrhmeo  24842  pi1buni  24938  minveclem3b  25326  uniioombllem2  25482  uniioombllem6  25487  vitali  25512  ellimc2  25776  limcflf  25780  taylfvallem  26263  taylf  26266  tayl0  26267  taylpfval  26270  xrlimcnp  26876  lrrecse  27854  ewlkle  29551  upgrewlkle2  29552  wlk1walk  29584  maprnin  32674  ordtprsval  33885  ordtprsuni  33886  ordtrestNEW  33888  ordtrest2NEWlem  33889  ordtrest2NEW  33890  ordtconnlem1  33891  xrge0iifhmeo  33903  eulerpartgbij  34340  eulerpartlemmf  34343  eulerpart  34350  ballotlemfrc  34495  cvmsss2  35251  cvmcov2  35252  mvrsval  35482  mpstval  35512  mclsind  35547  mthmpps  35559  dfon2lem4  35764  brapply  35916  neibastop1  36337  filnetlem3  36358  weiunfr  36445  bj-restn0  37068  bj-restuni  37075  ptrest  37603  heiborlem3  37797  heibor  37805  polvalN  39888  fnwe2lem2  43028  harval3  43515  superficl  43544  ssficl  43546  trficl  43646  onfrALTlem5  44520  onfrALTlem5VD  44862  fourierdlem48  46139  fourierdlem49  46140  sge0resplit  46391  hoiqssbllem3  46609  rngcvalALTV  48253  rhmsubcALTVlem1  48269  ringcvalALTV  48277  invfn  49019