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

Theorem iotaex 6466
Description: Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.) Remove dependency on ax-10 2137, ax-11 2154, ax-12 2171. (Revised by SN, 6-Nov-2024.)
Assertion
Ref Expression
iotaex (℩𝑥𝜑) ∈ V

Proof of Theorem iotaex
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 iotaval2 6461 . . . 4 ({𝑥𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2 vex 3447 . . . 4 𝑦 ∈ V
31, 2eqeltrdi 2846 . . 3 ({𝑥𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
43exlimiv 1933 . 2 (∃𝑦{𝑥𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5 iotanul2 6463 . . 3 (¬ ∃𝑦{𝑥𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6 0ex 5262 . . 3 ∅ ∈ V
75, 6eqeltrdi 2846 . 2 (¬ ∃𝑦{𝑥𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
84, 7pm2.61i 182 1 (℩𝑥𝜑) ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1541  wex 1781  wcel 2106  {cab 2713  Vcvv 3443  c0 4280  {csn 4584  cio 6443
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-nul 5261
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-sn 4585  df-pr 4587  df-uni 4864  df-iota 6445
This theorem is referenced by:  iota4an  6475  fvex  6852  riotaex  7313  erov  8749  iunfictbso  10046  isf32lem9  10293  sumex  15564  prodex  15782  pcval  16708  grpidval  18508  fn0g  18510  gsumvalx  18523  psgnfn  19274  psgnval  19280  dchrptlem1  26596  lgsdchrval  26686  lgsdchr  26687  nosupno  27035  nosupdm  27036  nosupbday  27037  nosupfv  27038  nosupres  27039  nosupbnd1lem1  27040  noinfno  27050  noinfdm  27051  noinffv  27053  bnj1366  33310  bj-finsumval0  35723  ellimciota  43787  fourierdlem36  44316  eubrdm  45202  dfatafv2ex  45377  afv2ex  45378  funressndmafv2rn  45387
  Copyright terms: Public domain W3C validator