![]() |
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 3515 | . . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
5 | 4 | biimpri 227 | . 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) |
6 | exsimpr 1864 | . 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) → ∃𝑥𝜑) | |
7 | 1, 5, 6 | mp2b 10 | 1 ⊢ ∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 ∃wex 1773 ∈ wcel 2098 Vcvv 3463 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-clel 2802 |
This theorem is referenced by: en0 9036 en0OLD 9037 en0r 9039 ensn1 9040 ensn1OLD 9041 0domg 9123 tz9.1 9752 cplem2 9913 karden 9918 pwmnd 18893 2lgslem1 27345 griedg0prc 29121 1loopgrvd2 29361 bnj150 34564 fnchoice 44456 nfermltl8rev 47145 nfermltl2rev 47146 nfermltlrev 47147 nn0mnd 47353 rrx2xpreen 47904 |
Copyright terms: Public domain | W3C validator |