![]() |
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 3496 | . 2 ⊢ ∃𝑥 𝑥 = 𝐴 |
3 | ceqsexv2d.3 | . . 3 ⊢ 𝜓 | |
4 | ceqsexv2d.2 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
5 | 3, 4 | mpbiri 258 | . 2 ⊢ (𝑥 = 𝐴 → 𝜑) |
6 | 2, 5 | eximii 1834 | 1 ⊢ ∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 = wceq 1537 ∃wex 1776 ∈ wcel 2106 Vcvv 3478 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-clel 2814 |
This theorem is referenced by: en0 9057 en0r 9059 ensn1 9060 0domg 9139 tz9.1 9767 cplem2 9928 karden 9933 pwmnd 18963 2lgslem1 27453 griedg0prc 29296 1loopgrvd2 29536 bnj150 34869 fnchoice 44967 nfermltl8rev 47667 nfermltl2rev 47668 nfermltlrev 47669 nn0mnd 48023 rrx2xpreen 48569 |
Copyright terms: Public domain | W3C validator |