![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > moanimv | Structured version Visualization version 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 1772 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | moanim 2369 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-12 1944 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-ex 1675 df-nf 1679 df-eu 2314 df-mo 2315 |
This theorem is referenced by: 2reuswap 3254 2reu5lem2 3258 funmo 5617 funcnv 5665 fncnv 5669 isarep2 5685 fnres 5714 mptfnf 5721 fnopabg 5723 fvopab3ig 5968 opabex 6159 fnoprabg 6424 ovidi 6442 ovig 6445 caovmo 6533 zfrep6 6788 oprabexd 6807 oprabex 6808 nqerf 9381 cnextfun 21128 perfdvf 22907 taylf 23365 2reuswap2 28173 abrexdomjm 28190 abrexdom 32102 2rmoswap 38643 |
Copyright terms: Public domain | W3C validator |