Theorem inex1 5253

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 5234	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2724	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3913	. . . . . . 7 ⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
5	4	bibi2i 337	. . . . . 6 ⊢ ((𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
6	5	albii 1820	. . . . 5 ⊢ (∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
7	3, 6	bitri 275	. . . 4 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
8	7	exbii 1849	. . 3 ⊢ (∃𝑥 𝑥 = (𝐴 ∩ 𝐵) ↔ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	2, 8	mpbir 231	. 2 ⊢ ∃𝑥 𝑥 = (𝐴 ∩ 𝐵)
10	9	issetri 3455	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2111  Vcvv 3436   ∩ cin 3896

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904

This theorem is referenced by:  inex2  5254  inex1g  5255  inuni  5286  onfr  6345  ssimaex  6907  exfo  7038  ofmres  7916  fipwuni  9310  fisn  9311  elfiun  9314  dffi3  9315  marypha1lem  9317  epfrs  9621  tcmin  9629  bnd2  9786  kmlem13  10054  brdom3  10419  brdom5  10420  brdom4  10421  fpwwe  10537  canthwelem  10541  pwfseqlem4  10553  ingru  10706  ltweuz  13868  elrest  17331  invfval  17666  isoval  17672  isofn  17682  zeroofn  17896  zerooval  17902  catcval  18007  isacs5lem  18451  isunit  20291  isrhm  20396  rhmfn  20414  rhmval  20415  rhmsubclem1  20600  2idlval  21188  pjfval  21643  psdmul  22081  fctop  22919  cctop  22921  ppttop  22922  epttop  22924  mretopd  23007  toponmre  23008  tgrest  23074  resttopon  23076  restco  23079  ordtbas2  23106  cnrest2  23201  cnpresti  23203  cnprest  23204  cnprest2  23205  cmpsublem  23314  cmpsub  23315  connsuba  23335  1stcrest  23368  subislly  23396  cldllycmp  23410  lly1stc  23411  txrest  23546  basqtop  23626  fbssfi  23752  trfbas2  23758  snfil  23779  fgcl  23793  trfil2  23802  cfinfil  23808  csdfil  23809  supfil  23810  zfbas  23811  fin1aufil  23847  fmfnfmlem3  23871  flimrest  23898  hauspwpwf1  23902  fclsrest  23939  tmdgsum2  24011  tsmsval2  24045  tsmssubm  24058  ustuqtop2  24157  restmetu  24485  isnmhm  24661  icopnfhmeo  24868  iccpnfhmeo  24870  xrhmeo  24871  pi1buni  24967  minveclem3b  25355  uniioombllem2  25511  uniioombllem6  25516  vitali  25541  ellimc2  25805  limcflf  25809  taylfvallem  26292  taylf  26295  tayl0  26296  taylpfval  26299  xrlimcnp  26905  lrrecse  27885  ewlkle  29584  upgrewlkle2  29585  wlk1walk  29617  maprnin  32714  ordtprsval  33931  ordtprsuni  33932  ordtrestNEW  33934  ordtrest2NEWlem  33935  ordtrest2NEW  33936  ordtconnlem1  33937  xrge0iifhmeo  33949  eulerpartgbij  34385  eulerpartlemmf  34388  eulerpart  34395  ballotlemfrc  34540  cvmsss2  35318  cvmcov2  35319  mvrsval  35549  mpstval  35579  mclsind  35614  mthmpps  35626  dfon2lem4  35828  brapply  35980  neibastop1  36403  filnetlem3  36424  weiunfr  36511  bj-restn0  37134  bj-restuni  37141  ptrest  37669  heiborlem3  37863  heibor  37871  polvalN  40014  fnwe2lem2  43154  harval3  43641  superficl  43670  ssficl  43672  trficl  43772  onfrALTlem5  44645  onfrALTlem5VD  44987  fourierdlem48  46262  fourierdlem49  46263  sge0resplit  46514  hoiqssbllem3  46732  rngcvalALTV  48375  rhmsubcALTVlem1  48391  ringcvalALTV  48399  invfn  49141