Theorem inex1 5288

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 5262	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2758	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3922	. . . . . . 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 3476	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2146  Vcvv 3457   ∩ cin 3905

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913

This theorem is used by:  inex2  5289  inex1g  5290  inuni  5322  onfr  6404  ssimaex  6970  exfo  7104  ofmres  7987  fipwuni  9393  fisn  9394  elfiun  9397  dffi3  9398  marypha1lem  9400  epfrs  9707  tcmin  9715  bnd2  9892  kmlem13  10162  brdom3  10527  brdom5  10528  brdom4  10529  fpwwe  10648  canthwelem  10652  pwfseqlem4  10664  ingru  10817  ltweuz  14017  elrest  17504  invfval  17840  isoval  17846  isofn  17856  zeroofn  18070  zerooval  18076  catcval  18181  isacs5lem  18625  isunit  20503  isrhm  20609  rhmfn  20636  rhmval  20638  rhmsubclem1  20836  2idlval  21442  pjfval  21908  psdmul  22381  fctop  23213  cctop  23215  ppttop  23216  epttop  23218  mretopd  23301  toponmre  23302  tgrest  23368  resttopon  23370  restco  23373  ordtbas2  23400  cnrest2  23495  cnpresti  23497  cnprest  23498  cnprest2  23499  cmpsublem  23608  cmpsub  23609  connsuba  23629  1stcrest  23662  subislly  23691  cldllycmp  23705  lly1stc  23706  txrest  23841  basqtop  23921  fbssfi  24047  trfbas2  24053  snfil  24074  fgcl  24088  trfil2  24097  cfinfil  24103  csdfil  24104  supfil  24105  zfbas  24106  fin1aufil  24142  fmfnfmlem3  24166  flimrest  24193  hauspwpwf1  24197  fclsrest  24234  tmdgsum2  24306  tsmsval2  24340  tsmssubm  24353  ustuqtop2  24452  restmetu  24780  isnmhm  24956  icopnfhmeo  25155  iccpnfhmeo  25157  xrhmeo  25158  pi1buni  25252  minveclem3b  25640  uniioombllem2  25795  uniioombllem6  25800  vitali  25825  ellimc2  26089  limcflf  26093  taylfvallem  26574  taylf  26577  tayl0  26578  taylpfval  26581  xrlimcnp  27186  lrrecse  28188  ewlkle  30015  upgrewlkle2  30016  wlk1walk  30048  maprnin  33148  ordtprsval  34374  ordtprsuni  34375  ordtrestNEW  34377  ordtrest2NEWlem  34378  ordtrest2NEW  34379  ordtconnlem1  34380  xrge0iifhmeo  34392  eulerpartgbij  34829  eulerpartlemmf  34832  eulerpart  34839  ballotlemfrc  34984  cvmsss2  35805  cvmcov2  35806  mvrsval  36036  mpstval  36066  mclsind  36101  mthmpps  36113  dfon2lem4  36315  brapply  36467  neibastop1  36929  filnetlem3  36950  weiunfr  37037  bj-restn0  37791  bj-restuni  37798  ptrest  38329  heiborlem3  38524  heibor  38532  polvalN  40739  fnwe2lem2  43838  harval3  44324  superficl  44353  ssficl  44355  trficl  44455  onfrALTlem5  45311  onfrALTlem5VD  45653  fourierdlem48  46928  fourierdlem49  46929  sge0resplit  47180  hoiqssbllem3  47398  rngcvalALTV  49089  rhmsubcALTVlem1  49105  ringcvalALTV  49113  invfn  49867