Theorem inex1 5273

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 5248	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2755	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3920	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 339	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1839	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 277	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1868	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 233	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3473	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 208   ∧ wa 399  ∀wal 1558   = wceq 1560  ∃wex 1799   ∈ wcel 2142  Vcvv 3454   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-in 3911

This theorem is referenced by:  inex2  5274  inex1g  5275  inuni  5306  onfr  6385  ssimaex  6952  exfo  7086  ofmres  7965  fipwuni  9372  fisn  9373  elfiun  9376  dffi3  9377  marypha1lem  9379  epfrs  9686  tcmin  9694  bnd2  9851  kmlem13  10119  brdom3  10485  brdom5  10486  brdom4  10487  fpwwe  10604  canthwelem  10608  pwfseqlem4  10620  ingru  10773  ltweuz  13974  elrest  17456  invfval  17792  isoval  17798  isofn  17808  zeroofn  18022  zerooval  18028  catcval  18133  isacs5lem  18577  isunit  20422  isrhm  20527  rhmfn  20548  rhmval  20549  rhmsubclem1  20735  2idlval  21321  pjfval  21758  psdmul  22231  fctop  23064  cctop  23066  ppttop  23067  epttop  23069  mretopd  23152  toponmre  23153  tgrest  23219  resttopon  23221  restco  23224  ordtbas2  23251  cnrest2  23346  cnpresti  23348  cnprest  23349  cnprest2  23350  cmpsublem  23459  cmpsub  23460  connsuba  23480  1stcrest  23513  subislly  23541  cldllycmp  23555  lly1stc  23556  txrest  23691  basqtop  23771  fbssfi  23897  trfbas2  23903  snfil  23924  fgcl  23938  trfil2  23947  cfinfil  23953  csdfil  23954  supfil  23955  zfbas  23956  fin1aufil  23992  fmfnfmlem3  24016  flimrest  24043  hauspwpwf1  24047  fclsrest  24084  tmdgsum2  24156  tsmsval2  24190  tsmssubm  24203  ustuqtop2  24302  restmetu  24630  isnmhm  24806  icopnfhmeo  25005  iccpnfhmeo  25007  xrhmeo  25008  pi1buni  25102  minveclem3b  25490  uniioombllem2  25645  uniioombllem6  25650  vitali  25675  ellimc2  25939  limcflf  25943  taylfvallem  26421  taylf  26424  tayl0  26425  taylpfval  26428  xrlimcnp  27033  lrrecse  28035  ewlkle  29806  upgrewlkle2  29807  wlk1walk  29839  maprnin  32933  ordtprsval  34215  ordtprsuni  34216  ordtrestNEW  34218  ordtrest2NEWlem  34219  ordtrest2NEW  34220  ordtconnlem1  34221  xrge0iifhmeo  34233  eulerpartgbij  34669  eulerpartlemmf  34672  eulerpart  34679  ballotlemfrc  34824  cvmsss2  35624  cvmcov2  35625  mvrsval  35855  mpstval  35885  mclsind  35920  mthmpps  35932  dfon2lem4  36134  brapply  36286  neibastop1  36719  filnetlem3  36740  weiunfr  36827  bj-restn0  37580  bj-restuni  37587  ptrest  38118  heiborlem3  38312  heibor  38320  polvalN  40529  fnwe2lem2  43628  harval3  44114  superficl  44143  ssficl  44145  trficl  44245  onfrALTlem5  45118  onfrALTlem5VD  45460  fourierdlem48  46728  fourierdlem49  46729  sge0resplit  46980  hoiqssbllem3  47198  rngcvalALTV  48887  rhmsubcALTVlem1  48903  ringcvalALTV  48911  invfn  49651