Theorem inex1 4727

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 4711	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2604	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3758	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 326	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1737	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 263	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1764	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 220	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3183	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173   ∩ cin 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547

This theorem is referenced by:  inex2  4728  inex1g  4729  inuni  4753  predasetex  5612  onfr  5680  ssimaex  6173  exfo  6285  ofmres  7055  fipwuni  8215  fisn  8216  elfiun  8219  dffi3  8220  marypha1lem  8222  epfrs  8490  tcmin  8500  bnd2  8639  kmlem13  8867  brdom3  9231  brdom5  9232  brdom4  9233  fpwwe  9347  canthwelem  9351  pwfseqlem4  9363  ingru  9516  ltweuz  12622  elrest  15911  invfval  16242  isoval  16248  isofn  16258  zerooval  16472  catcval  16569  isacs5lem  16992  isunit  18480  isrhm  18544  2idlval  19054  pjfval  19869  fctop  20618  cctop  20620  ppttop  20621  epttop  20623  mretopd  20706  toponmre  20707  tgrest  20773  resttopon  20775  restco  20778  ordtbas2  20805  cnrest2  20900  cnpresti  20902  cnprest  20903  cnprest2  20904  cmpsublem  21012  cmpsub  21013  consuba  21033  1stcrest  21066  subislly  21094  cldllycmp  21108  lly1stc  21109  txrest  21244  basqtop  21324  fbssfi  21451  trfbas2  21457  snfil  21478  fgcl  21492  trfil2  21501  cfinfil  21507  csdfil  21508  supfil  21509  zfbas  21510  fin1aufil  21546  fmfnfmlem3  21570  flimrest  21597  hauspwpwf1  21601  fclsrest  21638  tmdgsum2  21710  tsmsval2  21743  tsmssubm  21756  ustuqtop2  21856  metustfbas  22172  restmetu  22185  isnmhm  22360  icopnfhmeo  22550  iccpnfhmeo  22552  xrhmeo  22553  pi1buni  22648  minveclem3b  23007  uniioombllem2  23157  uniioombllem6  23162  vitali  23188  ellimc2  23447  limcflf  23451  taylfvallem  23916  taylf  23919  tayl0  23920  taylpfval  23923  xrlimcnp  24495  maprnin  28894  ordtprsval  29292  ordtprsuni  29293  ordtrestNEW  29295  ordtrest2NEWlem  29296  ordtrest2NEW  29297  ordtconlem1  29298  xrge0iifhmeo  29310  eulerpartgbij  29761  eulerpartlemmf  29764  eulerpart  29771  ballotlemfrc  29915  cvmsss2  30510  cvmcov2  30511  mvrsval  30656  mpstval  30686  mclsind  30721  mthmpps  30733  dfon2lem4  30935  brapply  31215  neibastop1  31524  filnetlem3  31545  bj-restn0  32224  bj-restuni  32231  ptrest  32578  heiborlem3  32782  heibor  32790  polvalN  34209  fnwe2lem2  36639  superficl  36891  ssficl  36893  trficl  36980  onfrALTlem5  37778  onfrALTlem5VD  38143  fourierdlem48  39047  fourierdlem49  39048  sge0resplit  39299  hoiqssbllem3  39514  ewlkle  40807  upgrewlkle2  40808  1wlk1walk  40843  rhmfn  41708  rhmval  41709  rngcvalALTV  41753  ringcvalALTV  41799  rhmsubclem1  41878  rhmsubcALTVlem1  41897