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

Theorem inex1 4994
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 4977 . . 3 𝑥𝑦(𝑦𝑥 ↔ (𝑦𝐴𝑦𝐵))
3 dfcleq 2800 . . . . 5 (𝑥 = (𝐴𝐵) ↔ ∀𝑦(𝑦𝑥𝑦 ∈ (𝐴𝐵)))
4 elin 3995 . . . . . . 7 (𝑦 ∈ (𝐴𝐵) ↔ (𝑦𝐴𝑦𝐵))
54bibi2i 328 . . . . . 6 ((𝑦𝑥𝑦 ∈ (𝐴𝐵)) ↔ (𝑦𝑥 ↔ (𝑦𝐴𝑦𝐵)))
65albii 1904 . . . . 5 (∀𝑦(𝑦𝑥𝑦 ∈ (𝐴𝐵)) ↔ ∀𝑦(𝑦𝑥 ↔ (𝑦𝐴𝑦𝐵)))
73, 6bitri 266 . . . 4 (𝑥 = (𝐴𝐵) ↔ ∀𝑦(𝑦𝑥 ↔ (𝑦𝐴𝑦𝐵)))
87exbii 1933 . . 3 (∃𝑥 𝑥 = (𝐴𝐵) ↔ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝐴𝑦𝐵)))
92, 8mpbir 222 . 2 𝑥 𝑥 = (𝐴𝐵)
109issetri 3404 1 (𝐴𝐵) ∈ V
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384  wal 1635   = wceq 1637  wex 1859  wcel 2156  Vcvv 3391  cin 3768
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776
This theorem is referenced by:  inex2  4995  inex1g  4996  inuni  5018  predasetex  5908  onfr  5976  ssimaex  6484  exfo  6599  ofmres  7394  fipwuni  8571  fisn  8572  elfiun  8575  dffi3  8576  marypha1lem  8578  epfrs  8854  tcmin  8864  bnd2  9003  kmlem13  9269  brdom3  9635  brdom5  9636  brdom4  9637  fpwwe  9753  canthwelem  9757  pwfseqlem4  9769  ingru  9922  ltweuz  12984  elrest  16293  invfval  16623  isoval  16629  isofn  16639  zerooval  16853  catcval  16950  isacs5lem  17374  isunit  18859  isrhm  18925  2idlval  19442  pjfval  20260  fctop  21022  cctop  21024  ppttop  21025  epttop  21027  mretopd  21110  toponmre  21111  tgrest  21177  resttopon  21179  restco  21182  ordtbas2  21209  cnrest2  21304  cnpresti  21306  cnprest  21307  cnprest2  21308  cmpsublem  21416  cmpsub  21417  connsuba  21437  1stcrest  21470  subislly  21498  cldllycmp  21512  lly1stc  21513  txrest  21648  basqtop  21728  fbssfi  21854  trfbas2  21860  snfil  21881  fgcl  21895  trfil2  21904  cfinfil  21910  csdfil  21911  supfil  21912  zfbas  21913  fin1aufil  21949  fmfnfmlem3  21973  flimrest  22000  hauspwpwf1  22004  fclsrest  22041  tmdgsum2  22113  tsmsval2  22146  tsmssubm  22159  ustuqtop2  22259  metustfbas  22575  restmetu  22588  isnmhm  22763  icopnfhmeo  22955  iccpnfhmeo  22957  xrhmeo  22958  pi1buni  23052  minveclem3b  23411  uniioombllem2  23564  uniioombllem6  23569  vitali  23594  ellimc2  23855  limcflf  23859  taylfvallem  24326  taylf  24329  tayl0  24330  taylpfval  24333  xrlimcnp  24909  ewlkle  26729  upgrewlkle2  26730  wlk1walk  26763  maprnin  29833  ordtprsval  30289  ordtprsuni  30290  ordtrestNEW  30292  ordtrest2NEWlem  30293  ordtrest2NEW  30294  ordtconnlem1  30295  xrge0iifhmeo  30307  eulerpartgbij  30759  eulerpartlemmf  30762  eulerpart  30769  ballotlemfrc  30913  cvmsss2  31579  cvmcov2  31580  mvrsval  31725  mpstval  31755  mclsind  31790  mthmpps  31802  dfon2lem4  32011  brapply  32366  neibastop1  32675  filnetlem3  32696  bj-restn0  33354  bj-restuni  33361  ptrest  33721  heiborlem3  33923  heibor  33931  polvalN  35685  fnwe2lem2  38122  superficl  38372  ssficl  38374  trficl  38461  onfrALTlem5  39255  onfrALTlem5VD  39615  fourierdlem48  40850  fourierdlem49  40851  sge0resplit  41102  hoiqssbllem3  41320  rhmfn  42486  rhmval  42487  rngcvalALTV  42529  ringcvalALTV  42575  rhmsubclem1  42654  rhmsubcALTVlem1  42672
  Copyright terms: Public domain W3C validator