![]() |
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.) |
Ref | Expression |
---|---|
ceqsexv2d.1 | ⊢ 𝐴 ∈ V |
ceqsexv2d.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
ceqsexv2d.3 | ⊢ 𝜓 |
Ref | Expression |
---|---|
ceqsexv2d | ⊢ ∃𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ceqsexv2d.3 | . 2 ⊢ 𝜓 | |
2 | ceqsexv2d.1 | . . . 4 ⊢ 𝐴 ∈ V | |
3 | ceqsexv2d.2 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | ceqsexv 3523 | . . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
5 | 4 | biimpri 227 | . 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) |
6 | exsimpr 1872 | . 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) → ∃𝑥𝜑) | |
7 | 1, 5, 6 | mp2b 10 | 1 ⊢ ∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∃wex 1781 ∈ wcel 2106 Vcvv 3474 |
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 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-clel 2810 |
This theorem is referenced by: en0 8998 en0OLD 8999 en0r 9001 ensn1 9002 ensn1OLD 9003 0domg 9085 tz9.1 9708 cplem2 9869 karden 9874 pwmnd 18795 2lgslem1 26826 griedg0prc 28450 1loopgrvd2 28689 bnj150 33782 fnchoice 43548 nfermltl8rev 46246 nfermltl2rev 46247 nfermltlrev 46248 nn0mnd 46425 rrx2xpreen 47117 |
Copyright terms: Public domain | W3C validator |