Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > moanimv | GIF 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 1461 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | moanim 2015 | 1 ⊢ (∃*𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 → ∃*𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 ∃*wmo 1942 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 662 ax-5 1376 ax-7 1377 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-8 1435 ax-10 1436 ax-11 1437 ax-i12 1438 ax-bndl 1439 ax-4 1440 ax-17 1459 ax-i9 1463 ax-ial 1467 ax-i5r 1468 |
This theorem depends on definitions: df-bi 115 df-nf 1390 df-sb 1686 df-eu 1944 df-mo 1945 |
This theorem is referenced by: mosubt 2769 2reuswapdc 2794 2rmorex 2796 mosubopt 4423 funmo 4937 funcnv 4980 fncnv 4985 isarep2 5006 fnres 5035 fnopabg 5042 fvopab3ig 5267 opabex 5406 fnoprabg 5622 ovidi 5639 ovig 5642 oprabexd 5774 oprabex 5775 th3qcor 6233 |
Copyright terms: Public domain | W3C validator |