![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ceqsexv | GIF version |
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) |
Ref | Expression |
---|---|
ceqsexv.1 | ⊢ 𝐴 ∈ V |
ceqsexv.2 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ceqsexv | ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1528 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | ceqsexv.1 | . 2 ⊢ 𝐴 ∈ V | |
3 | ceqsexv.2 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | ceqsex 2775 | 1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1353 ∃wex 1492 ∈ wcel 2148 Vcvv 2737 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-v 2739 |
This theorem is referenced by: ceqsex3v 2779 gencbvex 2783 sbhypf 2786 euxfr2dc 2922 inuni 4152 eqvinop 4240 onm 4398 uniuni 4448 opeliunxp 4678 elvvv 4686 rexiunxp 4765 imai 4980 coi1 5140 abrexco 5754 opabex3d 6116 opabex3 6117 mapsnen 6805 xpsnen 6815 xpcomco 6820 xpassen 6824 |
Copyright terms: Public domain | W3C validator |