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 1515 | . 2 ⊢ Ⅎ𝑥𝜓 | |
2 | ceqsexv.1 | . 2 ⊢ 𝐴 ∈ V | |
3 | ceqsexv.2 | . 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
4 | 1, 2, 3 | ceqsex 2759 | 1 ⊢ (∃𝑥(𝑥 = 𝐴 ∧ 𝜑) ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 = wceq 1342 ∃wex 1479 ∈ wcel 2135 Vcvv 2721 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-v 2723 |
This theorem is referenced by: ceqsex3v 2763 gencbvex 2767 sbhypf 2770 euxfr2dc 2906 inuni 4128 eqvinop 4215 onm 4373 uniuni 4423 opeliunxp 4653 elvvv 4661 rexiunxp 4740 imai 4954 coi1 5113 abrexco 5721 opabex3d 6081 opabex3 6082 mapsnen 6768 xpsnen 6778 xpcomco 6783 xpassen 6787 |
Copyright terms: Public domain | W3C validator |