Theorem iota2 6474

Description: The unique element such that 𝜑. (Contributed by Jeff Madsen, 1-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2016.)

Hypothesis

Ref	Expression
iota2.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
iota2	⊢ ((𝐴 ∈ 𝐵 ∧ ∃!𝑥𝜑) → (𝜓 ↔ (℩𝑥𝜑) = 𝐴))

Distinct variable groups:   𝑥,𝐴   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem iota2

Step	Hyp	Ref	Expression
1		elex 3452	. 2 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
2		simpl 483	. . 3 ⊢ ((𝐴 ∈ V ∧ ∃!𝑥𝜑) → 𝐴 ∈ V)
3		simpr 485	. . 3 ⊢ ((𝐴 ∈ V ∧ ∃!𝑥𝜑) → ∃!𝑥𝜑)
4		iota2.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	4	adantl 482	. . 3 ⊢ (((𝐴 ∈ V ∧ ∃!𝑥𝜑) ∧ 𝑥 = 𝐴) → (𝜑 ↔ 𝜓))
6		nfv 1921	. . . 4 ⊢ Ⅎ𝑥 𝐴 ∈ V
7		nfeu1 2593	. . . 4 ⊢ Ⅎ𝑥∃!𝑥𝜑
8	6, 7	nfan 1906	. . 3 ⊢ Ⅎ𝑥(𝐴 ∈ V ∧ ∃!𝑥𝜑)
9		nfvd 1922	. . 3 ⊢ ((𝐴 ∈ V ∧ ∃!𝑥𝜑) → Ⅎ𝑥𝜓)
10		nfcvd 2902	. . 3 ⊢ ((𝐴 ∈ V ∧ ∃!𝑥𝜑) → Ⅎ𝑥𝐴)
11	2, 3, 5, 8, 9, 10	iota2df 6472	. 2 ⊢ ((𝐴 ∈ V ∧ ∃!𝑥𝜑) → (𝜓 ↔ (℩𝑥𝜑) = 𝐴))
12	1, 11	sylan 586	1 ⊢ ((𝐴 ∈ 𝐵 ∧ ∃!𝑥𝜑) → (𝜓 ↔ (℩𝑥𝜑) = 𝐴))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∃!weu 2572  Vcvv 3431  ℩cio 6439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ral 3054  df-rex 3064  df-v 3433  df-un 3888  df-ss 3900  df-sn 4556  df-pr 4558  df-uni 4839  df-iota 6441

This theorem is referenced by:  iotan0  6475  pczpre  16809  pcdiv  16814  ringurd  20157  nosupno  27685  nosupfv  27688  noinfno  27700  noinffv  27703  bj-nuliota  37410  unirep  38081  presucmap  38862  ellimciota  46059