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 3493 | . . 3 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
5 | 4 | biimpri 227 | . 2 ⊢ (𝜓 → ∃𝑥(𝑥 = 𝐴 ∧ 𝜑)) |
6 | exsimpr 1873 | . 2 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) → ∃𝑥𝜑) | |
7 | 1, 5, 6 | mp2b 10 | 1 ⊢ ∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 Vcvv 3444 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-clel 2816 |
This theorem is referenced by: en0 8891 en0OLD 8892 en0r 8894 ensn1 8895 ensn1OLD 8896 0domg 8978 tz9.1 9599 cplem2 9760 karden 9765 pwmnd 18682 2lgslem1 26664 griedg0prc 27998 1loopgrvd2 28237 bnj150 33249 fnchoice 42967 nfermltl8rev 45634 nfermltl2rev 45635 nfermltlrev 45636 nn0mnd 45813 rrx2xpreen 46505 |
Copyright terms: Public domain | W3C validator |