| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > moanimv | Unicode version | ||
| Description: Introduction of a conjunct into at-most-one quantifier. (Contributed by NM, 23-Mar-1995.) |
| Ref | Expression |
|---|---|
| moanimv |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfv 1551 |
. 2
| |
| 2 | 1 | moanim 2128 |
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-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 |
| This theorem depends on definitions: df-bi 117 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 |
| This theorem is referenced by: mosubt 2950 2reuswapdc 2977 2rmorex 2979 mosubopt 4740 funmo 5286 funcnv 5335 fncnv 5340 isarep2 5361 fnres 5392 fnopabg 5399 fvopab3ig 5653 opabex 5808 fnoprabg 6046 ovidi 6064 ovig 6067 oprabexd 6212 oprabex 6213 th3qcor 6726 dvfgg 15160 |
| Copyright terms: Public domain | W3C validator |