Theorem inex1 5280

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 5254	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2756	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 4095	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 340	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1851	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 278	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1880	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 234	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3472	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2146  Vcvv 3453   ∩ cin 4091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5251

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-in 4093

This theorem is used by:  inex2  5281  inex1g  5282  inuni  5314  onfr  6408  ssimaex  6978  exfo  7113  ofmres  8003  fnwe2lem3  8157  fipwuni  9428  fisn  9429  elfiun  9432  dffi3  9433  marypha1lem  9435  epfrs  9742  tcmin  9750  bnd2  9966  kmlem13  10251  brdom3  10617  brdom5  10618  brdom4  10619  fpwwe  10741  canthwelem  10745  pwfseqlem4  10757  ingru  10910  ltweuz  14114  elrest  17610  invfval  17946  isoval  17952  isofn  17962  zeroofn  18176  zerooval  18182  catcval  18287  isacs5lem  18731  isunit  20615  isrhm  20721  rhmfn  20748  rhmval  20750  rhmsubclem1  20949  2idlval  21556  pjfval  22024  psdmul  22499  fctop  23334  cctop  23336  ppttop  23337  epttop  23339  mretopd  23422  toponmre  23423  tgrest  23489  resttopon  23491  restco  23494  ordtbas2  23521  cnrest2  23616  cnpresti  23618  cnprest  23619  cnprest2  23620  cmpsublem  23729  cmpsub  23730  connsuba  23750  1stcrest  23783  subislly  23812  cldllycmp  23826  lly1stc  23827  txrest  23962  basqtop  24042  fbssfi  24168  trfbas2  24174  snfil  24195  fgcl  24209  trfil2  24218  cfinfil  24224  csdfil  24225  supfil  24226  zfbas  24227  fin1aufil  24263  fmfnfmlem3  24287  flimrest  24314  hauspwpwf1  24318  fclsrest  24355  tmdgsum2  24427  tsmsval2  24461  tsmssubm  24474  ustuqtop2  24573  restmetu  24901  isnmhm  25077  icopnfhmeo  25276  iccpnfhmeo  25278  xrhmeo  25279  pi1buni  25373  minveclem3b  25761  uniioombllem2  25916  uniioombllem6  25921  vitali  25946  ellimc2  26209  limcflf  26213  taylfvallem  26697  taylf  26700  tayl0  26701  taylpfval  26704  xrlimcnp  27308  lrrecse  28340  ewlkle  30198  upgrewlkle2  30199  wlk1walk  30231  maprnin  33376  ordtprsval  34603  ordtprsuni  34604  ordtrestNEW  34606  ordtrest2NEWlem  34607  ordtrest2NEW  34608  ordtconnlem1  34609  xrge0iifhmeo  34621  eulerpartgbij  35057  eulerpartlemmf  35060  eulerpart  35067  ballotlemfrc  35212  weexenwe  35827  cvmsss2  36160  cvmcov2  36161  mvrsval  36391  mpstval  36421  mclsind  36456  mthmpps  36468  dfon2lem4  36675  brapply  36827  neibastop1  37274  filnetlem3  37295  weiunfr  37382  bj-restn0  38150  bj-restuni  38157  ptrest  38677  heiborlem3  38887  heibor  38895  polvalN  41102  harval3  44679  superficl  44708  ssficl  44710  trficl  44809  onfrALTlem5  45664  onfrALTlem5VD  46006  fourierdlem48  47303  fourierdlem49  47304  sge0resplit  47555  hoiqssbllem3  47773  rngcvalALTV  49501  rhmsubcALTVlem1  49517  ringcvalALTV  49525  invfn  50283