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 1421 | . 2 | |
2 | 1 | moanim 1974 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 wb 98 wmo 1901 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 df-eu 1903 df-mo 1904 |
This theorem is referenced by: mosubt 2718 2reuswapdc 2743 2rmorex 2745 mosubopt 4405 funmo 4917 funcnv 4960 fncnv 4965 isarep2 4986 fnres 5015 fnopabg 5022 fvopab3ig 5246 opabex 5385 fnoprabg 5602 ovidi 5619 ovig 5622 oprabexd 5754 oprabex 5755 th3qcor 6210 |
Copyright terms: Public domain | W3C validator |