Theorem inex1 5286

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

Syntax hints:   ↔ wb 209   ∧ wa 400  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143  Vcvv 3455   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912

This theorem is referenced by:  inex2  5287  inex1g  5288  inuni  5320  onfr  6400  ssimaex  6966  exfo  7100  ofmres  7977  fipwuni  9382  fisn  9383  elfiun  9386  dffi3  9387  marypha1lem  9389  epfrs  9696  tcmin  9704  bnd2  9875  kmlem13  10142  brdom3  10507  brdom5  10508  brdom4  10509  fpwwe  10626  canthwelem  10630  pwfseqlem4  10642  ingru  10795  ltweuz  13993  elrest  17475  invfval  17811  isoval  17817  isofn  17827  zeroofn  18041  zerooval  18047  catcval  18152  isacs5lem  18596  isunit  20451  isrhm  20557  rhmfn  20584  rhmval  20586  rhmsubclem1  20784  2idlval  21390  pjfval  21856  psdmul  22329  fctop  23161  cctop  23163  ppttop  23164  epttop  23166  mretopd  23249  toponmre  23250  tgrest  23316  resttopon  23318  restco  23321  ordtbas2  23348  cnrest2  23443  cnpresti  23445  cnprest  23446  cnprest2  23447  cmpsublem  23556  cmpsub  23557  connsuba  23577  1stcrest  23610  subislly  23638  cldllycmp  23652  lly1stc  23653  txrest  23788  basqtop  23868  fbssfi  23994  trfbas2  24000  snfil  24021  fgcl  24035  trfil2  24044  cfinfil  24050  csdfil  24051  supfil  24052  zfbas  24053  fin1aufil  24089  fmfnfmlem3  24113  flimrest  24140  hauspwpwf1  24144  fclsrest  24181  tmdgsum2  24253  tsmsval2  24287  tsmssubm  24300  ustuqtop2  24399  restmetu  24727  isnmhm  24903  icopnfhmeo  25102  iccpnfhmeo  25104  xrhmeo  25105  pi1buni  25199  minveclem3b  25587  uniioombllem2  25742  uniioombllem6  25747  vitali  25772  ellimc2  26036  limcflf  26040  taylfvallem  26521  taylf  26524  tayl0  26525  taylpfval  26528  xrlimcnp  27133  lrrecse  28135  ewlkle  29955  upgrewlkle2  29956  wlk1walk  29988  maprnin  33076  ordtprsval  34308  ordtprsuni  34309  ordtrestNEW  34311  ordtrest2NEWlem  34312  ordtrest2NEW  34313  ordtconnlem1  34314  xrge0iifhmeo  34326  eulerpartgbij  34762  eulerpartlemmf  34765  eulerpart  34772  ballotlemfrc  34917  cvmsss2  35766  cvmcov2  35767  mvrsval  35997  mpstval  36027  mclsind  36062  mthmpps  36074  dfon2lem4  36276  brapply  36428  neibastop1  36890  filnetlem3  36911  weiunfr  36998  bj-restn0  37752  bj-restuni  37759  ptrest  38290  heiborlem3  38484  heibor  38492  polvalN  40699  fnwe2lem2  43798  harval3  44284  superficl  44313  ssficl  44315  trficl  44415  onfrALTlem5  45271  onfrALTlem5VD  45613  fourierdlem48  46888  fourierdlem49  46889  sge0resplit  47140  hoiqssbllem3  47358  rngcvalALTV  49050  rhmsubcALTVlem1  49066  ringcvalALTV  49074  invfn  49828