Theorem inex1 5272

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 5253	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2722	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3930	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1819	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 275	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1848	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 231	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3466	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  Vcvv 3447   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921

This theorem is referenced by:  inex2  5273  inex1g  5274  inuni  5305  onfr  6371  ssimaex  6946  exfo  7077  ofmres  7963  fipwuni  9377  fisn  9378  elfiun  9381  dffi3  9382  marypha1lem  9384  epfrs  9684  tcmin  9694  bnd2  9846  kmlem13  10116  brdom3  10481  brdom5  10482  brdom4  10483  fpwwe  10599  canthwelem  10603  pwfseqlem4  10615  ingru  10768  ltweuz  13926  elrest  17390  invfval  17721  isoval  17727  isofn  17737  zeroofn  17951  zerooval  17957  catcval  18062  isacs5lem  18504  isunit  20282  isrhm  20387  rhmfn  20408  rhmval  20409  rhmsubclem1  20594  2idlval  21161  pjfval  21615  psdmul  22053  fctop  22891  cctop  22893  ppttop  22894  epttop  22896  mretopd  22979  toponmre  22980  tgrest  23046  resttopon  23048  restco  23051  ordtbas2  23078  cnrest2  23173  cnpresti  23175  cnprest  23176  cnprest2  23177  cmpsublem  23286  cmpsub  23287  connsuba  23307  1stcrest  23340  subislly  23368  cldllycmp  23382  lly1stc  23383  txrest  23518  basqtop  23598  fbssfi  23724  trfbas2  23730  snfil  23751  fgcl  23765  trfil2  23774  cfinfil  23780  csdfil  23781  supfil  23782  zfbas  23783  fin1aufil  23819  fmfnfmlem3  23843  flimrest  23870  hauspwpwf1  23874  fclsrest  23911  tmdgsum2  23983  tsmsval2  24017  tsmssubm  24030  ustuqtop2  24130  restmetu  24458  isnmhm  24634  icopnfhmeo  24841  iccpnfhmeo  24843  xrhmeo  24844  pi1buni  24940  minveclem3b  25328  uniioombllem2  25484  uniioombllem6  25489  vitali  25514  ellimc2  25778  limcflf  25782  taylfvallem  26265  taylf  26268  tayl0  26269  taylpfval  26272  xrlimcnp  26878  lrrecse  27849  ewlkle  29533  upgrewlkle2  29534  wlk1walk  29567  maprnin  32654  ordtprsval  33908  ordtprsuni  33909  ordtrestNEW  33911  ordtrest2NEWlem  33912  ordtrest2NEW  33913  ordtconnlem1  33914  xrge0iifhmeo  33926  eulerpartgbij  34363  eulerpartlemmf  34366  eulerpart  34373  ballotlemfrc  34518  cvmsss2  35261  cvmcov2  35262  mvrsval  35492  mpstval  35522  mclsind  35557  mthmpps  35569  dfon2lem4  35774  brapply  35926  neibastop1  36347  filnetlem3  36368  weiunfr  36455  bj-restn0  37078  bj-restuni  37085  ptrest  37613  heiborlem3  37807  heibor  37815  polvalN  39899  fnwe2lem2  43040  harval3  43527  superficl  43556  ssficl  43558  trficl  43658  onfrALTlem5  44532  onfrALTlem5VD  44874  fourierdlem48  46152  fourierdlem49  46153  sge0resplit  46404  hoiqssbllem3  46622  rngcvalALTV  48253  rhmsubcALTVlem1  48269  ringcvalALTV  48277  invfn  49019