![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ceqsexv | Unicode version |
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.) |
Ref | Expression |
---|---|
ceqsexv.1 |
![]() ![]() ![]() ![]() |
ceqsexv.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ceqsexv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1538 |
. 2
![]() ![]() ![]() ![]() | |
2 | ceqsexv.1 |
. 2
![]() ![]() ![]() ![]() | |
3 | ceqsexv.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | ceqsex 2787 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 1457 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-nf 1471 df-sb 1773 df-clab 2174 df-cleq 2180 df-clel 2183 df-v 2751 |
This theorem is referenced by: ceqsex3v 2791 gencbvex 2795 sbhypf 2798 euxfr2dc 2934 inuni 4167 eqvinop 4255 onm 4413 uniuni 4463 opeliunxp 4693 elvvv 4701 rexiunxp 4781 imai 4996 coi1 5156 abrexco 5773 opabex3d 6136 opabex3 6137 mapsnen 6825 xpsnen 6835 xpcomco 6840 xpassen 6844 |
Copyright terms: Public domain | W3C validator |