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

Theorem iotaex 6521
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 2130, ax-11 2147, ax-12 2167. (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 6516 . . . 4 ({𝑥𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦)
2 vex 3475 . . . 4 𝑦 ∈ V
31, 2eqeltrdi 2837 . . 3 ({𝑥𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
43exlimiv 1926 . 2 (∃𝑦{𝑥𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
5 iotanul2 6518 . . 3 (¬ ∃𝑦{𝑥𝜑} = {𝑦} → (℩𝑥𝜑) = ∅)
6 0ex 5307 . . 3 ∅ ∈ V
75, 6eqeltrdi 2837 . 2 (¬ ∃𝑦{𝑥𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V)
84, 7pm2.61i 182 1 (℩𝑥𝜑) ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1534  wex 1774  wcel 2099  {cab 2705  Vcvv 3471  c0 4323  {csn 4629  cio 6498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4909  df-iota 6500
This theorem is referenced by:  iota4an  6530  fvex  6910  riotaex  7380  erov  8833  iunfictbso  10138  isf32lem9  10385  sumex  15667  prodex  15884  pcval  16813  grpidval  18621  fn0g  18623  gsumvalx  18636  psgnfn  19456  psgnval  19462  dchrptlem1  27210  lgsdchrval  27300  lgsdchr  27301  nosupno  27649  nosupdm  27650  nosupbday  27651  nosupfv  27652  nosupres  27653  nosupbnd1lem1  27654  noinfno  27664  noinfdm  27665  noinffv  27667  bnj1366  34460  bj-finsumval0  36764  ellimciota  45002  fourierdlem36  45531  eubrdm  46418  dfatafv2ex  46593  afv2ex  46594  funressndmafv2rn  46603
  Copyright terms: Public domain W3C validator