Theorem inex1 5221

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 5205	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2815	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 4169	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 340	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1820	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 277	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1848	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 233	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3510	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 208   ∧ wa 398  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114  Vcvv 3494   ∩ cin 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943

This theorem is referenced by:  inex2  5222  inex1g  5223  inuni  5246  predasetex  6163  onfr  6230  ssimaex  6748  exfo  6871  ofmres  7685  fipwuni  8890  fisn  8891  elfiun  8894  dffi3  8895  marypha1lem  8897  epfrs  9173  tcmin  9183  bnd2  9322  kmlem13  9588  brdom3  9950  brdom5  9951  brdom4  9952  fpwwe  10068  canthwelem  10072  pwfseqlem4  10084  ingru  10237  ltweuz  13330  elrest  16701  invfval  17029  isoval  17035  isofn  17045  zerooval  17259  catcval  17356  isacs5lem  17779  isunit  19407  isrhm  19473  2idlval  20006  pjfval  20850  fctop  21612  cctop  21614  ppttop  21615  epttop  21617  mretopd  21700  toponmre  21701  tgrest  21767  resttopon  21769  restco  21772  ordtbas2  21799  cnrest2  21894  cnpresti  21896  cnprest  21897  cnprest2  21898  cmpsublem  22007  cmpsub  22008  connsuba  22028  1stcrest  22061  subislly  22089  cldllycmp  22103  lly1stc  22104  txrest  22239  basqtop  22319  fbssfi  22445  trfbas2  22451  snfil  22472  fgcl  22486  trfil2  22495  cfinfil  22501  csdfil  22502  supfil  22503  zfbas  22504  fin1aufil  22540  fmfnfmlem3  22564  flimrest  22591  hauspwpwf1  22595  fclsrest  22632  tmdgsum2  22704  tsmsval2  22738  tsmssubm  22751  ustuqtop2  22851  restmetu  23180  isnmhm  23355  icopnfhmeo  23547  iccpnfhmeo  23549  xrhmeo  23550  pi1buni  23644  minveclem3b  24031  uniioombllem2  24184  uniioombllem6  24189  vitali  24214  ellimc2  24475  limcflf  24479  taylfvallem  24946  taylf  24949  tayl0  24950  taylpfval  24953  xrlimcnp  25546  ewlkle  27387  upgrewlkle2  27388  wlk1walk  27420  maprnin  30467  ordtprsval  31161  ordtprsuni  31162  ordtrestNEW  31164  ordtrest2NEWlem  31165  ordtrest2NEW  31166  ordtconnlem1  31167  xrge0iifhmeo  31179  eulerpartgbij  31630  eulerpartlemmf  31633  eulerpart  31640  ballotlemfrc  31784  cvmsss2  32521  cvmcov2  32522  mvrsval  32752  mpstval  32782  mclsind  32817  mthmpps  32829  dfon2lem4  33031  brapply  33399  neibastop1  33707  filnetlem3  33728  bj-restn0  34384  bj-restuni  34391  ptrest  34906  heiborlem3  35106  heibor  35114  polvalN  37056  fnwe2lem2  39700  harval3  39953  superficl  39975  ssficl  39977  trficl  40063  onfrALTlem5  40925  onfrALTlem5VD  41268  fourierdlem48  42488  fourierdlem49  42489  sge0resplit  42737  hoiqssbllem3  42955  rhmfn  44238  rhmval  44239  rngcvalALTV  44281  ringcvalALTV  44327  rhmsubclem1  44406  rhmsubcALTVlem1  44424