| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ceqsexv2d | Structured version Visualization version GIF version | ||
| Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016.) Shorten, reduce dv conditions. (Revised by Wolf Lammen, 5-Jun-2025.) (Proof shortened by SN, 5-Jun-2025.) |
| Ref | Expression |
|---|---|
| ceqsexv2d.1 | ⊢ 𝐴 ∈ V |
| ceqsexv2d.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
| ceqsexv2d.3 | ⊢ 𝜓 |
| Ref | Expression |
|---|---|
| ceqsexv2d | ⊢ ∃𝑥𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ceqsexv2d.1 | . . 3 ⊢ 𝐴 ∈ V | |
| 2 | 1 | isseti 3498 | . 2 ⊢ ∃𝑥 𝑥 = 𝐴 |
| 3 | ceqsexv2d.3 | . . 3 ⊢ 𝜓 | |
| 4 | ceqsexv2d.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
| 5 | 3, 4 | mpbiri 258 | . 2 ⊢ (𝑥 = 𝐴 → 𝜑) |
| 6 | 2, 5 | eximii 1837 | 1 ⊢ ∃𝑥𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∃wex 1779 ∈ wcel 2108 Vcvv 3480 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-clel 2816 |
| This theorem is referenced by: en0 9058 en0r 9060 ensn1 9061 0domg 9140 tz9.1 9769 cplem2 9930 karden 9935 pwmnd 18950 2lgslem1 27438 griedg0prc 29281 1loopgrvd2 29521 bnj150 34890 fnchoice 45034 nfermltl8rev 47729 nfermltl2rev 47730 nfermltlrev 47731 nn0mnd 48095 rrx2xpreen 48640 |
| Copyright terms: Public domain | W3C validator |