Theorem inex1 5287

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 5268	. . 3 ⊢ ∃𝑥∀𝑦(𝑦 ∈ 𝑥 ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
3		dfcleq 2728	. . . . 5 ⊢ (𝑥 = (𝐴 ∩ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝑥 ↔ 𝑦 ∈ (𝐴 ∩ 𝐵)))
4		elin 3942	. . . . . . 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 3478	1 ⊢ (𝐴 ∩ 𝐵) ∈ V

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108  Vcvv 3459   ∩ cin 3925

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933

This theorem is referenced by:  inex2  5288  inex1g  5289  inuni  5320  onfr  6391  ssimaex  6964  exfo  7095  ofmres  7983  fipwuni  9438  fisn  9439  elfiun  9442  dffi3  9443  marypha1lem  9445  epfrs  9745  tcmin  9755  bnd2  9907  kmlem13  10177  brdom3  10542  brdom5  10543  brdom4  10544  fpwwe  10660  canthwelem  10664  pwfseqlem4  10676  ingru  10829  ltweuz  13979  elrest  17441  invfval  17772  isoval  17778  isofn  17788  zeroofn  18002  zerooval  18008  catcval  18113  isacs5lem  18555  isunit  20333  isrhm  20438  rhmfn  20459  rhmval  20460  rhmsubclem1  20645  2idlval  21212  pjfval  21666  psdmul  22104  fctop  22942  cctop  22944  ppttop  22945  epttop  22947  mretopd  23030  toponmre  23031  tgrest  23097  resttopon  23099  restco  23102  ordtbas2  23129  cnrest2  23224  cnpresti  23226  cnprest  23227  cnprest2  23228  cmpsublem  23337  cmpsub  23338  connsuba  23358  1stcrest  23391  subislly  23419  cldllycmp  23433  lly1stc  23434  txrest  23569  basqtop  23649  fbssfi  23775  trfbas2  23781  snfil  23802  fgcl  23816  trfil2  23825  cfinfil  23831  csdfil  23832  supfil  23833  zfbas  23834  fin1aufil  23870  fmfnfmlem3  23894  flimrest  23921  hauspwpwf1  23925  fclsrest  23962  tmdgsum2  24034  tsmsval2  24068  tsmssubm  24081  ustuqtop2  24181  restmetu  24509  isnmhm  24685  icopnfhmeo  24892  iccpnfhmeo  24894  xrhmeo  24895  pi1buni  24991  minveclem3b  25380  uniioombllem2  25536  uniioombllem6  25541  vitali  25566  ellimc2  25830  limcflf  25834  taylfvallem  26317  taylf  26320  tayl0  26321  taylpfval  26324  xrlimcnp  26930  lrrecse  27901  ewlkle  29585  upgrewlkle2  29586  wlk1walk  29619  maprnin  32708  ordtprsval  33949  ordtprsuni  33950  ordtrestNEW  33952  ordtrest2NEWlem  33953  ordtrest2NEW  33954  ordtconnlem1  33955  xrge0iifhmeo  33967  eulerpartgbij  34404  eulerpartlemmf  34407  eulerpart  34414  ballotlemfrc  34559  cvmsss2  35296  cvmcov2  35297  mvrsval  35527  mpstval  35557  mclsind  35592  mthmpps  35604  dfon2lem4  35804  brapply  35956  neibastop1  36377  filnetlem3  36398  weiunfr  36485  bj-restn0  37108  bj-restuni  37115  ptrest  37643  heiborlem3  37837  heibor  37845  polvalN  39924  fnwe2lem2  43075  harval3  43562  superficl  43591  ssficl  43593  trficl  43693  onfrALTlem5  44567  onfrALTlem5VD  44909  fourierdlem48  46183  fourierdlem49  46184  sge0resplit  46435  hoiqssbllem3  46653  rngcvalALTV  48240  rhmsubcALTVlem1  48256  ringcvalALTV  48264  invfn  49000