MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  inex1 Structured version   Visualization version   GIF version

Theorem inex1 5220
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.
StepHypRef Expression
1 inex1.1 . . . 4 𝐴 ∈ V
21zfauscl 5204 . . 3 𝑥𝑦(𝑦𝑥 ↔ (𝑦𝐴𝑦𝐵))
3 dfcleq 2815 . . . . 5 (𝑥 = (𝐴𝐵) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (𝐴𝐵)))
4 elin 4168 . . . . . . 7 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴𝑦𝐵))
54bibi2i 340 . . . . . 6 ((𝑦𝑥𝑦 ∈ (𝐴𝐵)) ↔ (𝑦𝑥 ↔ (𝑦𝐴𝑦𝐵)))
65albii 1816 . . . . 5 (∀𝑦(𝑦𝑥𝑦 ∈ (𝐴𝐵)) ↔ ∀𝑦(𝑦𝑥 ↔ (𝑦𝐴𝑦𝐵)))
73, 6bitri 277 . . . 4 (𝑥 = (𝐴𝐵) ↔ ∀𝑦(𝑦𝑥 ↔ (𝑦𝐴𝑦𝐵)))
87exbii 1844 . . 3 (∃𝑥 𝑥 = (𝐴𝐵) ↔ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝐴𝑦𝐵)))
92, 8mpbir 233 . 2 𝑥 𝑥 = (𝐴𝐵)
109issetri 3510 1 (𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  wal 1531   = wceq 1533  wex 1776  wcel 2110  Vcvv 3494  cin 3934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3942
This theorem is referenced by:  inex2  5221  inex1g  5222  inuni  5245  predasetex  6162  onfr  6229  ssimaex  6747  exfo  6870  ofmres  7684  fipwuni  8889  fisn  8890  elfiun  8893  dffi3  8894  marypha1lem  8896  epfrs  9172  tcmin  9182  bnd2  9321  kmlem13  9587  brdom3  9949  brdom5  9950  brdom4  9951  fpwwe  10067  canthwelem  10071  pwfseqlem4  10083  ingru  10236  ltweuz  13328  elrest  16700  invfval  17028  isoval  17034  isofn  17044  zerooval  17258  catcval  17355  isacs5lem  17778  isunit  19406  isrhm  19472  2idlval  20005  pjfval  20849  fctop  21611  cctop  21613  ppttop  21614  epttop  21616  mretopd  21699  toponmre  21700  tgrest  21766  resttopon  21768  restco  21771  ordtbas2  21798  cnrest2  21893  cnpresti  21895  cnprest  21896  cnprest2  21897  cmpsublem  22006  cmpsub  22007  connsuba  22027  1stcrest  22060  subislly  22088  cldllycmp  22102  lly1stc  22103  txrest  22238  basqtop  22318  fbssfi  22444  trfbas2  22450  snfil  22471  fgcl  22485  trfil2  22494  cfinfil  22500  csdfil  22501  supfil  22502  zfbas  22503  fin1aufil  22539  fmfnfmlem3  22563  flimrest  22590  hauspwpwf1  22594  fclsrest  22631  tmdgsum2  22703  tsmsval2  22737  tsmssubm  22750  ustuqtop2  22850  restmetu  23179  isnmhm  23354  icopnfhmeo  23546  iccpnfhmeo  23548  xrhmeo  23549  pi1buni  23643  minveclem3b  24030  uniioombllem2  24183  uniioombllem6  24188  vitali  24213  ellimc2  24474  limcflf  24478  taylfvallem  24945  taylf  24948  tayl0  24949  taylpfval  24952  xrlimcnp  25545  ewlkle  27386  upgrewlkle2  27387  wlk1walk  27419  maprnin  30466  ordtprsval  31161  ordtprsuni  31162  ordtrestNEW  31164  ordtrest2NEWlem  31165  ordtrest2NEW  31166  ordtconnlem1  31167  xrge0iifhmeo  31179  eulerpartgbij  31630  eulerpartlemmf  31633  eulerpart  31640  ballotlemfrc  31784  cvmsss2  32521  cvmcov2  32522  mvrsval  32752  mpstval  32782  mclsind  32817  mthmpps  32829  dfon2lem4  33031  brapply  33399  neibastop1  33707  filnetlem3  33728  bj-restn0  34380  bj-restuni  34387  ptrest  34890  heiborlem3  35090  heibor  35098  polvalN  37040  fnwe2lem2  39649  harval3  39902  superficl  39924  ssficl  39926  trficl  40012  onfrALTlem5  40874  onfrALTlem5VD  41217  fourierdlem48  42438  fourierdlem49  42439  sge0resplit  42687  hoiqssbllem3  42905  rhmfn  44188  rhmval  44189  rngcvalALTV  44231  ringcvalALTV  44277  rhmsubclem1  44356  rhmsubcALTVlem1  44374
  Copyright terms: Public domain W3C validator